[SVA] Getting SVA-OPTCOV-LMFA warning due to the the bounded temporal consequent expression

SystemVerilog
1

Hi,

I had one assertion as below

assert property(sig1,sig2);
@(posedge test_clk)
$rose(sig1) |-> ##[1:20000] sig2;
endproperty
The above causing a warning as Warning-[SVA-OPTCOV-LMFA] Large memory footprint assertion

So I had replaced as below with goto operator. Is the below code is suggestable or any better way we have to detect consequent assertion:

//CP6:
property assert_chk(sig1,sig2);
@(posedge test_clk)
$rose(sig1) |-> ##1 sig2[->1]; //This property checks in consequent for assert of signal
endproperty

Thank you
Bharath

2

In reply to BhaRath@Intel:


// Your original syntax is wrong.  Should be 
property p (sig1,sig2);
  @(posedge clk)
  $rose(sig1) |-> ##[1:20000] sig2;
endproperty
  
  ap_p: assert property(@ (posedge clk) p(a, b)); 
// or this 
  ap_p2: assert property(@ (posedge clk) $rose(a) |->  ##[1:20000] b);

// the following is probably better, but it has a different meaning 
// it depends on your specs 
$rose(sig1) |-> ##1 sig2[->1];

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers: