OR Construct basics in Concurrent Assertions

SystemVerilog
,
1

Hi all ,

I am trying to understand the basics of “or” construct and have following Code :: EDA_LINK

The antecedent is ::


a[ *1:2 ]  ##1  b  is  equivalent  to  (  a  ## 1  b  )  or  (  a  ##1  a   ##1  b  )  

As  a  result  the  resultant  expression  is  :: (  (  a  ## 1  b  )  or  (  a  ##1  a   ##1  b  )  )  |->  c  ;

I am confused why does the 1st assertion Pass at TIME : 500 instead of TIME : 400


 Let's  assume  (  a  ## 1  b  )   is  Thread 1  and   (  a  ##1  a   ##1  b  )  is  Thread2 

 At  TIME : 300  ,  ' a  '  is  True  hence  both  Threads  start  evaluation .

 As ' b ' is True  at  TIME : 400  ,  Thread1  succeeds  .

 However  as  ' c ' is  also  True  at  TIME : 400  ,  why  doesn't  the  assertion  Pass  at  TIME : 400  ?

 As  per   ::  seq1  or  seq2  ,  match  occurs  whenever  either  of  the  2  sequences  complete  .

 So  I  expected  Pass  at  TIME : 400  as   Thread1  was  successful  

 i.e  antecedent  was  a  match  and  then  the  consequent  ' c '  was  True  at  TIME : 400  too .

 Thread2  succeeds  at  TIME : 500  (  as  expected  )  and  the  assertion  passes  at  TIME : 500 .

NOTE :: Using first_match in antecedent makes the assertion Pass at TIME : 400 as per expectation .

2

In reply to hisingh:

If a multi-threaded sequence is used in an antecedent (e.g., a ##1 b[*1:3] ##1 c |-> d), then all threads must be tested with its consequent for the assertion to terminate as successful.

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) https://rb.gy/cwy7nb
  3. Papers:
3

In reply to ben@SystemVerilog.us:

In reply to hisingh:
then all threads must be tested with its consequent for the assertion to terminate as successful.

Could you please elaborate on this ?

I am having a hard time of making sense of it logically .

For the Attempt1 at TIME : 300 , the “or” construct is behaving as “and” construct as it waits for longer sequence ( a ##1 a ##1 b |-> c ) to complete .

In the 2 paths possible ( Path1 :: Thread1 |-> c and Path2 :: Thread2 |-> c )

why is taking the longer path instead of the shorter one ?

4

In reply to hisingh:


a[*1:2]  ##1 b |-> c; // is  equivalent  to  
(a ##1 b )  or  (a ##1 a ##1 b)  |-> c; // also equivalent to 
((a ##1 b ) |-> c) and ((a ##1 a ##1 b)  |-> c);
 Thread1 |-> c and  Thread2 |-> c; // YES
  1. At each clocking event the two threads start at the same time.
  2. All threads of the antecedent must be tested.
  3. An antecedent thread can be a no-match (yielding vacuity “true vacuously” for that thread)
  4. For an assertion to PASS, there can be no failure in any of the attempted threads.
  5. For a nonvacuous PASS, at least one of the threads in nonvacuous.

If you are really serious about understanding these notions, I stronglyurge you to study my paper: -Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy

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/

5

In reply to ben@SystemVerilog.us:

Hi Ben ,

Along with your paper I went through the following ::

(1) SNUG09 paper "If Chained Implications in Properties Weren’t So Hard, They’d be Easy " by Don Mills

(2) VA_LINK1

(3) VA_LINK2

I have a better understanding of the Question I posted at the top and understand the O/P

However if I do a slight modification to the Sequence Expression .


sequence  ant_seq ;

 //   Attached  a  Subroutine  within  an  expression  in  a  ' sequence '  
 
 (  (  a[ *1:2 ]  ##1  b  ) , $display(" TIME : %0t  Antecedent  is  True " , $time ) ) ; 

  endsequence

[ Q ] When does the $display() execute ?

    **How  do  I  expand  the  above  expression  ::**

    Would  it  be  interpreted  as  ::


 (    ( a  ##1  b  )      ,  $display(" TIME : %0t  Antecedent  is  True " , $time ) )   or

 ( ( a  ##1  a  ##1  b  ) ,  $display(" TIME : %0t  Antecedent  is  True " , $time ) )

I have the code :: EDA_LINK2

Why do I observe 2 displays at TIME : 400 ?

Thread1 has Non - Vacuous Pass so I understand the attempt at TIME : 300 is a success . However I don’t get the 2nd $display() .

6

In reply to hisingh:

[ Q ] When does the $display() execute ?

[Ben] What you have is (sequence_expr {, sequence_match_item})
The sequence_match_item} is executed if the endpoint of sequence_expr is a match

How do I expand the above expression ::
Would it be interpreted as ::
( ( a ##1 b ) , $display(" TIME : %0t Antecedent is True " , $time ) ) or
( ( a ##1 a ##1 b ) , $display(" TIME : %0t Antecedent is True " , $time ) )

YES. Thr thread viewer helps in understanding what is going on
Thread viewer image http://systemverilog.us/vf/abc_or_aabc.png

Why do I observe 2 displays at TIME : 400 ?

Because you are running the property ab twice, once in the assertion and the other in the cover. You don’t need the cover. If you comment it out you get


 a_property : assert  property ( ab ) else  $display(" TIME : %0t  AB  FAIL " , $time , ) ;  
// c_property : cover   property ( ab )  $display(" TIME : %0t  AB  PASS " , $time ) ; 
  TIME : 400  Antecedent  is  True 
#  TIME : 500  Antecedent  is  True 
#  TIME : 500  Antecedent  is  True 
#  TIME : 700  AB  FAIL

1871×841 117 KB

7

In reply to hisingh:

Just adding a note for future reference

Even if I were to use “first_match” in property ab i.e


property  ab ;
  
    @( posedge clk )  first_match( ant_seq )  |->  c ; 

  endproperty

We still Observe the $display() execute Twice due to same reason as mentioned by Ben .