raviji
June 25, 2020, 12:59pm
1
Hello SVA Experts,
The design state machine is having lets say 4 states, S1, S2, S3 and S4.
From S1 I can reach S2, S3 or S4 (Only 1 of them shall be True at any given time)
S1 to S2 is single clk cycle state transition.
S1 to S3/S4 may be multiple clock Cycles (this can vary).
I have coded initially as below.
property S1_2_S2_S3_S4_CHECKS;
@(posedge clks) disable iff(~POR_N)
(state === S1) |=> (state === S2) || (state === S3) || (state === S4);
endproperty
option1: This passes for all cases.
(state === S1) |->##[1:$] (state === S2) || (state === S3) || (state === S4);
option2 :
first_match((state === S1) |->##[1:$] (state === S2) || (state === S3) || (state === S4));
Please suggest if these options are right to use.
Also there is a very common requirement that when reset is applied, there is a default state say S1 in the above case. As there is no clock involved how do we write an assertion for this?
Thanks
ben2
June 25, 2020, 8:42pm
2
In reply to raviji :
You need to use the sequential or operator.
property S1_2_S2_S3_S4_CHECKS;
@(posedge clks) disable iff(!POR_N)
state === S1 |=> state === S2 or
##[0:$] (state === S3) || (state === S4);
endproperty
ap_reset2s1: assert property(@ (posedge clk) // synchronous
!POR_N |=> state === S1);
always_comb if(!POR_N) state === S1; // asynchronous
NOTES
There is NO need for a first_match() in an antecendent when there is only ONE thread
first_match((state === S1) |-> // NO TO THIS!!!
On logical operations use the logical operators. Thus,
!POR_N // YES TO THIS
~POR_N // NOT recommended, as it implies that POR_N is a vector> 1bit
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
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 978-1539769712
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
SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy
SVA: Package for dynamic and range delays and repeats | Verification Academy
SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
mbhat
July 17, 2020, 9:25pm
3
In reply to ben@SystemVerilog.us :
Hi Ben, Raviji,
This assertion will not fail if the state transition does not take place from S1 to any of the states because of ##[0:$]. It appears like the only time the assertion fails if the transition from S1 to S2 takes more than 1 clock cycle. Please correct me if I am wrong.
ben2
July 17, 2020, 9:47pm
4
In reply to ManjunathBhat :
You would need the strong operator
state === S1 |=> strong (state === S2 or
##[0:$] (state === S3) || (state === S4));
mbhat
July 17, 2020, 10:35pm
5
In reply to ben@SystemVerilog.us :
In reply to ManjunathBhat :
You would need the strong operator
state === S1 |=> strong (state === S2 or
##[0:$] (state === S3) || (state === S4));
Thanks Ben.