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.

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.

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.

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.

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

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

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.