seq1 @(posedge clk_event)
$past(a==2’d2) && (a==2’d1) //make sure “a” has transitioned from 2->1
seq2 @(posedge clk_event)
$past(a==2’d1) && (a==2’d1) && $rose(B) //make sure when “a” is 1 at that time B has 0->1 transition
seq_3 seq1 ##[3:18] seq2
property check1;
@(posedge clk_event)
// seq_3 |-> [3:18] $rose(B) // To catch the 2nd pulse in B when a==1 and there was a transition 2 to 1 on "a"
The above seq_3 should have been success on the 6th clk_event after seq1
success (seq1 will be success once a transition from 2->1,
the same clock). But I am seeing seq_3 is only giving success when it completes
18 cycle because the subsequence seq2 is detecting only 2nd $rose(b).
I am thinking some issue on ##[3:18] used in between seq1 and seq2 for seq3, what does it imply when subsequences are separated with a range of ##?
Could you please suggest whats going wrong here?
[Ben] Your assertion looks like this when expanded:
$past(a==2'd2) && (a==2'd1) ##[3:18] $past(a==2'd1) && (a==2'd1) && $rose(B) |-> [3:18] $rose(B);
The antecedent has multiple threads, and All threads of an antecedent must be checked before the assertion completes, unless it fails.
You need a first_match; thus,
property check1;
@(posedge clk_event) first_match(seq_3) |-> [3:18] $rose(B);
endproperty
Other potential issues,
$past(a==2'd2) && (a==2'd1) //make sure "a" has transitioned from 2->1
##[3:18]
// $past(a==2'd1) && // [Ben] probably not needed. DO want a to stay at 1? if so, use the repeat operator
(a==2'd1) && $rose(B) // //make sure when "a" is 1 at that time B has 0->1 transition
|-> [3:18] $rose(B); // another rose of B
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115