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 #1292

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

Added by Joel Holdsworth 10 months ago. Updated 4 months ago.

Status:
Feature
Priority:
Normal
Assignee:
-
Category:
Unsupported
% Done:

0%


Description

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

History

#1 Updated by John Coiner 10 months ago

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.

#2 Updated by Joel Holdsworth 10 months ago

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.

#3 Updated by Wilson Snyder 10 months ago

  • Status changed from New to Confirmed

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.

#4 Updated by Joel Holdsworth 10 months ago

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.

#5 Updated by Stefan Wallentowitz 9 months ago

Hi,

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

Cheers, Stefan

#6 Updated by Joel Holdsworth 9 months ago

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

Joel

#7 Updated by Wilson Snyder 4 months ago

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

#8 Updated by Wilson Snyder 4 months ago

  • Status changed from Confirmed to Feature

Also available in: Atom