Project

General

Profile

[logo] 
 
Home
News
Activity
About/Contact
Major Tools
  Dinotrace
  Verilator
  Verilog-mode
  Verilog-Perl
Other Tools
  BugVise
  CovVise
  Force-Gate-Sim
  Gspice
  IPC::Locker
  Rsvn
  SVN::S4
  Voneline
  WFH
General Info
  Papers

Issue #785

Support for SystemVerilog assertions

Added by Alex Solomatnikov about 5 years ago. Updated over 1 year ago.

Status:
Closed
Priority:
Normal
Assignee:
Category:
Unsupported
% Done:

0%


Description

Change log says:

Verilator 3.860 2014-05-11
PSL is no longer supported, please use System Verilog assertions.

However, verilator errors out even for simple single cycle assertion:

   assert property (@(posedge clk) !(buf_en0 && buf_we0 && buf_en1 && buf_we1 && (buf_ind0 == buf_ind1)))
     else
       $error( "SVA ERROR: both write ports write to the index=%h", buf_ind0 );

Error:

%Error: ....v:1184: syntax error, unexpected assert

Slightly more complex assertion (single cycle after reset):

   assert property (@(posedge clk) $fell(rst) |-> !(buf_en0 && buf_we0 && buf_en1 && buf_we1 && (buf_ind0 == buf_ind1)))
     else
       $error( "SVA ERROR: both write ports write to the index=%h", buf_ind0 );

Produces 2 errors:

%Error: ....v:1184: syntax error, unexpected assert
%Error: ....v:1184: Unsupported or unknown PLI call: $fell

Related issues

Duplicated by Issue #1290: scr1 test suite: assert properties don't work Closed

History

#1 Updated by Wilson Snyder about 5 years ago

  • Category set to Unsupported
  • Status changed from New to Feature

Verilator supports concurrent SVA assertions. e.g.

always @ (posedge clk) begin
    AssertionFalse1: assert !(buf_en0 && buf_we0 && buf_en1 && buf_we1 && (buf_ind0 == buf_ind1)) else $error( "SVA ERROR: both write ports write to the index=%h", buf_ind0 );
 end

It could probably support "assert property" where the syntax is very limited to the PSL subset. I'll take this as the request of this bug.

$fell etc are a pain and unlikely to be any time soon.

#2 Updated by John Coiner over 1 year ago

  • Assignee set to John Coiner

I'll have a fix for this shortly.

Still NOT supported will be:

  • "|->" syntax
  • "##" syntax
  • referencing named properties in the assert
  • asserts without a sensitivity list. (I don't think there's a fundamental difficulty with this one, I'm just not doing it yet.)

#3 Updated by John Coiner over 1 year ago

  • Duplicated by Issue #1290: scr1 test suite: assert properties don't work added

#4 Updated by John Coiner over 1 year ago

UPDATE: there IS a fundamental difficulty supporting unclocked combinational concurrent asserts -- they're not allowed by the verilog spec.

We will support concurrent asserts that omit the sensitivity list, and thus depend on a prior declaration of a default clock. That will work for 'assert property' like it already does for 'cover property'.

#5 Updated by John Coiner over 1 year ago

Here's the fix.

commit c8cf2afb15860722e19c4ea6dd7ca0bc74010fac (HEAD -> master, origin/master, origin/HEAD) Author: Wilson Snyder <> Date: Sun Mar 11 10:37:20 2018 -0400

Support assert properties, bug785, bug1290.

#6 Updated by John Coiner over 1 year ago

  • Status changed from Feature to Closed

#7 Updated by John Coiner over 1 year ago

Fixed in git towards 3.922

Also available in: Atom