Alternative to throughout via Consecutive Repetition

SystemVerilog
,
1

I have following code using " throughout " operator :: EDA_LINK

I am curious to know if there is an alternative solution to the “throughout” operator using Consecutive Repetition Operator *[ m ] ??

By default the “throughout” operator checks that both LHS and RHS must meet their requirement during the interval

Is it possible to check this via it’s alternative ?

2

In reply to hisingh:
The throughout operator specifies that a signal (expression) must hold throughout a sequence.

( b throughout R ) is equivalent to ( b [*0:$] intersect R )

For example, in the following handshake example, a req is honored with an acknowledge within the next 4 cycles. The ack is then followed at a later time by a done control signal. However, there is one additional requirement that throughout the time between the ack and done an enable signal must be asserted to drive a tri-state bus. That assertion can be expressed as follows.

ap_handshake : assert property (
       $rose(req) |-> ##[1:4] enable throughout (ack ##[1:$] done));
//Same as 
   $rose(req) |-> ##[1:4] enable[*0:$] intersect (ack ##[1:$] done));

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3

In reply to ben@SystemVerilog.us:

Ben , I was actually looking for a ( crude ) solution without any operator ( within , intersect etc. )

I ended up coding the following :: EDA_throughout_ALT

For stimulus via +define+M2 I observe the same O/P as the original code ( using throughout )

However for +define+M1 due to Vacuous pass there is No assertion Failure at TIME : 70 .

I tried using strong operator in consequent of property ’ ab ’ but it throws Compilation Error .
**
Any suggestion on how Vacuous Pass of antecedent in property ’ checkMode ’ could
make the assertion FAIL ?**

4

In reply to hisingh:
COMMENTS:

  1. YOUR ISSUE: with (seq1 |-> seq2 |-> seq3) then
    If seq1 is a NO MATCH, then assertion is vacuous.
    If seq1 IS A MATCH and seq2 is a NO MATCH then assertion is vacuous
    This is because seq2 |-> seq3 is a property where seq2 is an antecedent
  2. ALTERNATE SOLUTIONS: One solution is to use the ONE antecedent. Thus,
ap_OK_mode: assert property(@ (posedge clk)
$fell( bMode )  ##0 (!bMode) [*4]  |->
##2  (dack_ == 0  && oe_ == 0) [*4]);

Another solution is to use the implies property operator

ap_OK2_mode : assert property(@ (posedge clk)
@ ( posedge  clk )   $fell( bMode )  implies  checkbMode );
// Note: LHS of the implies starts in the SAME cycle as the LHS
  1. STYLE:
  • 4. Way to many unnecessary declarations (sequences and properties).
    It makes it harder to read.
    5. If you reuse declared properties or sequences, use a prefix notation to identify the type. Some people use p_ for properties, s_ or q_ for sequences. I don’t care what notation you use, but be consistent throughout the project.
    6. Way to many character spaces and lines spaces; it makes the code harder to read.

FULL CODE and results :


module  Fig6_29_ALT2 ;
  bit  clk,  bMode ,  dack_, oe_ ;  
  sequence  data_transfer;
    ##2  ( ( dack_ == 0 )  && ( oe_ == 0 ) ) [*4]; 
  endsequence

 //  Declared  property  since  we  use  Implication  N  Sequences  can't  have  Implication Operator  !!  
  property  checkbMode ;
    ( ! bMode  ) [*4]  |->  data_transfer;     
  endproperty

  property  ab ;
    @ ( posedge  clk )   $fell( bMode )  |->  checkbMode;
  endproperty

  ap_BAD_mode: assert property(@ (posedge clk)  $fell( bMode )  |-> 
  ( ! bMode  ) [*4]  |-> ##2  ( ( dack_ == 0 )  && ( oe_ == 0 ) ) [*4]);   

  ap_OK_mode: assert property(@ (posedge clk)  
     $fell( bMode )  ##0 (!bMode) [*4]  |-> 
               ##2  (dack_ == 0  && oe_ == 0) [*4]); 
               
  ap_OK2_mode : assert property(@ (posedge clk) 
     @ ( posedge  clk )   $fell( bMode )  implies  checkbMode );  
     // Note: LHS of the implies starts in the SAME cycle as the LHS

ASSERT: Error: ASRT_0005 testbench.sv(19): Assertion “ap_BAD_mode” FAILED at time: 230ns (23 clk), scope: Fig6_29_ALT2, start-time: 180ns (18 clk)

ASSERT: Error: ASRT_0005 testbench.sv(22): Assertion “ap_OK_mode” FAILED at time: 230ns (23 clk), scope: Fig6_29_ALT2, start-time: 180ns (18 clk)

ASSERT: Error: ASRT_0005 testbench.sv(26): Assertion “ap_OK2_mode” FAILED at time: 230ns (23 clk), scope: Fig6_29_ALT2, start-time: 180ns (18 clk)

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/