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

scr1 test suite: |-> and |=> operators are unsupported in assertions #1292

Closed
veripoolbot opened this issue Mar 11, 2018 · 7 comments
Closed

scr1 test suite: |-> and |=> operators are unsupported in assertions #1292

veripoolbot opened this issue Mar 11, 2018 · 7 comments

Comments

@veripoolbot
Copy link
Contributor

@veripoolbot veripoolbot commented Mar 11, 2018


Author Name: Joel Holdsworth
Original Redmine Issue: 1292 from https://www.veripool.org


Code like this fails to build:

MYTEST : assert property (
  @(negedge clk) disable iff (~rst)
  a |-> b
  ) else $error("MYTEST failed");

with the message "syntax error, unexpected |->, expecting ')'".

@veripoolbot
Copy link
Contributor Author

@veripoolbot veripoolbot commented Mar 13, 2018


Original Redmine Comment
Author Name: John Coiner (@jcoiner)
Original Date: 2018-03-13T00:51:47Z


Verilator does not support the "|->" or "|=>" operators or the sequence expression ("##") operator.

In general, Verilator's going to have a difficult time supporting anything that can't be converted to a traditional synthesizable always block, which is how it handles "assert property" internally.

IIUC "|->" is purely combinational, in which case, the code you posted could be rewritten as:

MYTEST : assert property (
@(negedge clk) disable iff (~rst)
(a ? b : 1'b1)
) else $error("MYTEST failed");

(Is that really equivalent? I haven't used these operators.) If so you could add parser support for "|->" and convert it to the plain old ternary somewhere along the pipeline, maybe in V3Assert.cpp where the 'assert property' gets converted to a plain old always block.

"|=>" can be converted internally to a combination of "|->" and "##" according to http://www.project-veripage.com/sva_12.php

To support "##" you'd have to generate some state variables and a clocking pipeline. It's not impossible, it's just code.

@veripoolbot
Copy link
Contributor Author

@veripoolbot veripoolbot commented Mar 13, 2018


Original Redmine Comment
Author Name: Joel Holdsworth
Original Date: 2018-03-13T01:19:50Z


70% of the asserts in scr1 use "|->", so just having that one implemented would cut down the ifdefs (and increase the verification) quite a bit.

@veripoolbot
Copy link
Contributor Author

@veripoolbot veripoolbot commented Mar 13, 2018


Original Redmine Comment
Author Name: Wilson Snyder (@wsnyder)
Original Date: 2018-03-13T01:33:00Z


Joel, perhaps you'd like to try a fix? First make a test case (see internals.txt), then parse it, then finally upgrade V3Assert to convert to understandable internal syntax. We can provide more details if you want.

@veripoolbot
Copy link
Contributor Author

@veripoolbot veripoolbot commented Mar 13, 2018


Original Redmine Comment
Author Name: Joel Holdsworth
Original Date: 2018-03-13T03:23:26Z


I'd certainly like to help. I'm on a specific mission right now, so it might take a while for me to get around to it, but you've been really helpful, so I will try to contribute when I can.

@veripoolbot
Copy link
Contributor Author

@veripoolbot veripoolbot commented Apr 17, 2018


Original Redmine Comment
Author Name: Stefan Wallentowitz (@wallento)
Original Date: 2018-04-17T11:20:29Z


Hi,

I would be happy to contribute on that one. Joel, did you start already? If so, can you please contact me (stefan@wallentowitz.de) to coordinate?

Cheers,
Stefan

@veripoolbot
Copy link
Contributor Author

@veripoolbot veripoolbot commented Apr 17, 2018


Original Redmine Comment
Author Name: Joel Holdsworth
Original Date: 2018-04-17T14:50:00Z


Hi Stefan, I didn't look at the issue yet. Go ahead if you want to add support.

Joel

@veripoolbot
Copy link
Contributor Author

@veripoolbot veripoolbot commented Oct 5, 2018


Original Redmine Comment
Author Name: Wilson Snyder (@wsnyder)
Original Date: 2018-10-05T00:28:31Z


Note git master now supports $past() which may help getting support for some of these.

PeterMonsson added a commit to PeterMonsson/verilator that referenced this issue Dec 23, 2019
PeterMonsson added a commit to PeterMonsson/verilator that referenced this issue Dec 23, 2019
wsnyder pushed a commit that referenced this issue Sep 10, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked pull requests

Successfully merging a pull request may close this issue.

1 participant
You can’t perform that action at this time.