Multiple consequdn

SystemVerilog
,
1

I have assertion where for one antecedent state A there are two possible ways to reach state B .
Way one is timeout through time p. And another is if we see rise in signal q.
Can I wrote a assertion saying

property multi_conseq;
@(posedge clk) disable iff(rst)
(st==A) |-> (#p || ##[0:$]$rose(q)) ##1 (st==B);
endproperty
assert properrt(multi_conseq) ;

Am I writing it correct way,
Please correct me if I am wrong

2

In reply to Satputesb:
Two solutions, one for the static delay and another one for the dynamic delay.
The sva_delay_repeat_range_pkg is available in my signature below.


// Compile  sva_delay_repeat_range_pkg.sv before the module 
module m; 
  import sva_delay_repeat_range_pkg::*; // for use in dynamic delaya
  typedef enum {A, B} st_e;
  st_e st; 
  bit clk, rst, q; 
  int delay=5;
  // Way one is timeout through STATIC time p. And another is if we see rise in signal q.
  let p=4; 
  ap_stAB_static: assert property(@ (posedge clk) 
    disable iff(rst)
    st==A |-> (##p st==8) or  ($rose(q)[->1] ##1 st==B));   

 // If the delay is dynamic, use the package
 /* Application:  $rose(a)  |-> q_dynamic_delay(d1) ##0 my_sequence;
    ap_dyn_delay: assert property(@ (posedge clk) 
       $rose(a) |-> q_dynamic_delay(d1) ##0 my_sequence);  */ 
   ap_stAB_dynamic: assert property(@ (posedge clk) 
       disable iff(rst)
       st==A |-> (q_dynamic_delay(delay) ##0 st==8) or  ($rose(q)[->1] ##1 st==B));      

endmodule : m

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:

a. Is it possible to write it in a manner that by chance state is shifted to st=b without timeout p or without q is asserted , and thus assertion shows failure?
b. Is it possible to write (#p st==8) or ($rose(q)[->1] in antecedent?

4

In reply to Timus:

I don’t understand what you ant in your “a” question.
Yes on the “b” question, but what are your requirement?

5

In reply to ben@SystemVerilog.us:

In part a. I mean to say that assertion should fail if it is forced to move to next state without both the conditions met ie without the timeout or without arrival of signal q.
. For both part this failure criteria is the same requirment

6

In reply to ben@SystemVerilog.us:

is it good idea to write
in static delay case
st==A |-> (#p st==8) or ($rose(q)[->1] ##1 st==B));

as
(st ==A ) ##1 ((#p) or ($rose(q)[->1] ##1)) |=> st==B

7

In reply to Timus:
You mean


// This 
st==A |-> (##p st==B) or ($rose(q)[->1] ##1 st==B));

//as
st==A ##p or $rose(q)[->1] ##1 1 |->  st==B;

The difference is vacuity. If the antecedent is a no match the assertion fails.

8

In reply to ben@SystemVerilog.us:

In reply to Satputesb:
Two solutions, one for the static delay and another one for the dynamic delay.
The sva_delay_repeat_range_pkg is available in my signature below.


// Compile  sva_delay_repeat_range_pkg.sv before the module 
module m; 
import sva_delay_repeat_range_pkg::*; // for use in dynamic delaya
typedef enum {A, B} st_e;
st_e st; 
bit clk, rst, q; 
int delay=5;
// Way one is timeout through STATIC time p. And another is if we see rise in signal q.
let p=4; 
ap_stAB_static: assert property(@ (posedge clk) 
disable iff(rst)
st==A |-> (##p st==8) or  ($rose(q)[->1] ##1 st==B));   
// If the delay is dynamic, use the package
/* Application:  $rose(a)  |-> q_dynamic_delay(d1) ##0 my_sequence;
ap_dyn_delay: assert property(@ (posedge clk) 
$rose(a) |-> q_dynamic_delay(d1) ##0 my_sequence);  */ 
ap_stAB_dynamic: assert property(@ (posedge clk) 
disable iff(rst)
st==A |-> (q_dynamic_delay(delay) ##0 st==8) or  ($rose(q)[->1] ##1 st==B));      
endmodule : m

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 - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

This assertion with static time delay is failing
ap_stAB_static: assert property(@ (posedge clk)
disable iff(rst)
st==A |-> (##p st==8) or ($rose(q)[->1] ##1 st==B));

at time p even if q is asserted before the timeout . Error says offending st == B

9

In reply to Timus:
Check your testbench. It works as intended.

1834×821 151 KB

http://systemverilog.us/vf/temp928.sv

1834×821 151 KB