Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for SystemVerilog assertions #785

Closed
veripoolbot opened this issue Jun 10, 2014 · 5 comments
Closed

Support for SystemVerilog assertions #785

veripoolbot opened this issue Jun 10, 2014 · 5 comments
Assignees
Labels
resolution: fixed Closed; fixed type: feature-IEEE Request to add new feature, described in IEEE 1800

Comments

@veripoolbot
Copy link
Contributor


Author Name: Alex Solomatnikov
Original Redmine Issue: 785 from https://www.veripool.org

Original Assignee: John Coiner (@jcoiner)


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

@veripoolbot
Copy link
Contributor Author


Original Redmine Comment
Author Name: Wilson Snyder (@wsnyder)
Original Date: 2014-06-10T21:17:45Z


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.

@veripoolbot
Copy link
Contributor Author


Original Redmine Comment
Author Name: John Coiner (@jcoiner)
Original Date: 2018-03-09T21:46:11Z


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.)

@veripoolbot
Copy link
Contributor Author


Original Redmine Comment
Author Name: John Coiner (@jcoiner)
Original Date: 2018-03-10T18:33:49Z


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'.

@veripoolbot
Copy link
Contributor Author


Original Redmine Comment
Author Name: John Coiner (@jcoiner)
Original Date: 2018-03-11T14:56:08Z


Here's the fix.

commit c8cf2af (HEAD -> master, origin/master, origin/HEAD)
Author: Wilson Snyder wsnyder@wsnyder.org
Date: Sun Mar 11 10:37:20 2018 -0400

 Support assert properties, #�, #�.

@veripoolbot
Copy link
Contributor Author


Original Redmine Comment
Author Name: John Coiner (@jcoiner)
Original Date: 2018-03-12T23:45:34Z


Fixed in git towards 3.922

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
resolution: fixed Closed; fixed type: feature-IEEE Request to add new feature, described in IEEE 1800
Projects
None yet
Development

No branches or pull requests

2 participants