# Assertion failing to check all cases **URL:** \ **Category:** SystemVerilog\ **Tags:** SystemVerilog\ **Created:** [June 9, 2022, 3:13pm UTC](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509 "2022-06-09T15:13:30Z")\ **Posts on this page:** 10\ **Page:** 1
**Author:** ![John\_Canfield](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/j/d78d45/32.png) [@John\_Canfield](https://verificationacademy.com/forums/u/John_Canfield)\ **Post date:** [June 9, 2022, 3:13pm UTC](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/1 "2022-06-09T15:13:30Z")
Hello, I am an SVA beginner and I haven’t been able to figure out this odd (to me!) behavior. Any insights appreciated! Whenever state changes, I simply want to check that b is 0 at that instant (preponed value fine). This probably seems weird, but I don’t have access to the clock in this case. With the option 1 line uncommented below, the assertion works as I expect and runs successfully at every state change where state isn’t 00 (at times 1us, 2us and 3us). But, when I uncomment option 2 line instead (which I thought would have the same functionality) the assertion finishes only once (at 1us) and doesn’t check at 2us and 3us. Any idea why? ```verilog module top; logic [2:0] state=3'b001; logic b = 0; initial begin #1us; state = 3'b010; #1us state = 3'b011; #1us; state = 3'b100; #1us; $finish; end property myprop; @(state[2], state[1], state[0]) (state!=3'b00, $display("checking")) |-> (b==1'b0); // option 1 - checks all state changes //(state!=3'b00) |-> (b==1'b0); // option 2 - only checks first state change? endproperty assert property (myprop) $display("passed at %t",$realtime); else $display("failed at %t",$realtime); endmodule ``` Link to this example on edaplayground: [assertion problem with single event assertion - EDA Playground](https://www.edaplayground.com/x/E7MA) \*\*Running with option 1: \*\* xcelium\> run checking passed at 1000 checking passed at 2000 checking passed at 3000 Simulation complete via $finish(1) at time 4 US + 0 ./testbench.sv:15 $finish; \*\*Running with option 2: \*\* xcelium\> run passed at 1000 Simulation complete via $finish(1) at time 4 US + 0 ./testbench.sv:15 $finish; xcelium\> exit TOOL: xrun 20.09-s003: Exiting on Jun 09, 2022 at 11:07:19 EDT (total: 00:00:02) ---
**Author:** ![user49](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/user49/32/1084_2.png) [@user49](https://verificationacademy.com/forums/u/user49)\ **Post date:** [June 9, 2022, 4:53pm UTC](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/2 "2022-06-09T16:53:55Z")
_In reply to [John Canfield](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509):_ If you have a clock that changes the values of the states, then the clocking event should be that clock. If you are talking about an asynchronous state machine, then your @(state!=3’b00) means that the clocking event for the assertion is whenever states changes from 0 to a value unequal to 0 (i.e., 1, 2,…7), or vice versa. In other words, the @(state!=3’b00) has an event when the expression (state!=3’b00) transitions to 1 or transitions to 0. If that expression stalls at 0 ot 1, then thre is no clocking event. Ben Cohen [http://www.systemverilog.us/](http://www.systemverilog.us/) [ben@systemverilog.us](mailto: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](https://rb.gy/a89jlh) 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](https://rb.gy/9tcbhl) - Real Chip Design and Verification Using Verilog and VHDL($3) [https://rb.gy/cwy7nb](https://rb.gy/cwy7nb) - A Pragmatic Approach to VMM Adoption [http://SystemVerilog.us/vf/VMM/VMM\_pdf\_release070506.zip](http://SystemVerilog.us/vf/VMM/VMM_pdf_release070506.zip) [http://SystemVerilog.us/vf/VMM/VMM\_code\_release\_071806.tar](http://SystemVerilog.us/vf/VMM/VMM_code_release_071806.tar) 1. Papers: - Understanding the SVA Engine, [Verification Horizons - July 2020 | Verification Academy](https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2) - Reflections on Users’ Experiences with SVA [Reflections on Users’ Experiences with SVA | Verification Horizons - March 2022 | Verification Academy](https://verificationacademy.com/verification-horizons/march-2022-volume-18-issue-1/reflections-on-users-experiences-with-systemverilog-assertions-sva) - SVA Alternative for Complex Assertions [Verification Horizons - March 2018 Issue | Verification Academy](https://verificationacademy.com/news/verification-horizons-march-2018-issue) - SVA in a UVM Class-based Environment [SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy](https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment) Udemy courses by Srinivasan Venkataramanan ([http://cvcblr.com/home.html](http://cvcblr.com/home.html)) [https://www.udemy.com/course/sva-basic/](https://www.udemy.com/course/sva-basic/) [https://www.udemy.com/course/sv-pre-uvm/](https://www.udemy.com/course/sv-pre-uvm/) ---
**Author:** ![John\_Canfield](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/j/d78d45/32.png) [@John\_Canfield](https://verificationacademy.com/forums/u/John_Canfield)\ **Post date:** [June 9, 2022, 6:13pm UTC](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/3 "2022-06-09T18:13:54Z")
Thank you sir, that is insightful. I assume the behavior you describe occurs because I don’t have a defined posedge clk for the property? In my property: ```verilog property myprop; @(state[2], state[1], state[0]) (state!=3'b00) |-> (b==1'b0); endproperty ``` I thought the @(state[2], state[1], state[0]) would establish the clocking (essentially a clock event any time any one of those signals changed state)? I guess that is not the case? Also, any idea why the property _does_ seem to finish on any state change when the seemingly superfluous $display statement is added to it? Shouldn’t your argument still hold true - that it should only get a clocking even on a transition out of state in or out of state==0? I think I need to purchase your book! ---
**Author:** ![John\_Canfield](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/j/d78d45/32.png) [@John\_Canfield](https://verificationacademy.com/forums/u/John_Canfield)\ **Post date:** [June 9, 2022, 7:19pm UTC](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/4 "2022-06-09T19:19:38Z")
Also, why does the assertion execute/finish at t=1us, when the state is changing from 1 to 2 at which time the expression (state!=3’b000) should be constantly equal to 1? ---
**Author:** ![user49](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/user49/32/1084_2.png) [@user49](https://verificationacademy.com/forums/u/user49)\ **Post date:** [June 9, 2022, 7:33pm UTC](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/5 "2022-06-09T19:33:09Z")
_In reply to [John Canfield](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/4):_ > I thought the @(state[2], state[1], state[0]) would establish the clocking (essentially a clock event any time any one of those signals changed state)? I guess that is not the case? It is the case, per 1800’2017 9.4.2.1 Event OR operator > Also, any idea why the property does seem to finish on any state change when the seemingly superfluous $display statement is added to it? > Shouldn’t your argument still hold true - that it should only get a clocking even on a transition out of state in or out of state==0? It does. Note: #1us state=3’b001; #1us state = 3’b010; At the 2us, when state transitions to 3’b010 the sampling value of state is 3’b001. > **[EDA Playground](https://www.edaplayground.com/x/MJk9)** > > Edit, save, simulate, synthesize SystemVerilog, Verilog, VHDL and other HDLs from your web browser. ---
**Author:** ![John\_Canfield](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/j/d78d45/32.png) [@John\_Canfield](https://verificationacademy.com/forums/u/John_Canfield)\ **Post date:** [June 10, 2022, 12:16pm UTC](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/6 "2022-06-10T12:16:06Z")
Thank you for the help, but I still don’t think I understand. In the following example, why does **mypropGOOD** work (finishes at 1us, 2us, 3us, 4us) but **mypropBAD** does not (finishes ONLY at 1us)?: > **[EDA Playground](https://www.edaplayground.com/x/m2Ym)** > > Edit, save, simulate, synthesize SystemVerilog, Verilog, VHDL and other HDLs from your web browser. ```verilog module top; logic [2:0] state = 3'b001; logic b = 0; initial begin #1us state = 3'b010; #1us state = 3'b011; #1us state = 3'b100; #1us state = 3'b101; #1us $finish; end // doesn't work (I think) property mypropBAD; @(state[2], state[1], state[0]) (state!=3'b000) |-> (b==1'b0); endproperty pbad: assert property (mypropBAD) $display("mypropBAD passed at %t",$realtime); else $display("mypropBAD failed at %t",$realtime); // works property mypropGOOD; @(state[2], state[1], state[0]) (state!=3'b000) |-> (b==1'b0, $system("") ); endproperty pgood: assert property (mypropGOOD) $display("mypropGOOD passed at %t",$realtime); else $display("mypropGOOD failed at %t",$realtime); endmodule ``` Simulator Output for above: ```verilog mypropGOOD passed at 1000 mypropBAD passed at 1000 mypropGOOD passed at 2000 [why didn't mypropBAD finish here too?] mypropGOOD passed at 3000 [why didn't mypropBAD finish here too?] mypropGOOD passed at 4000 [why didn't mypropBAD finish here too?] ``` Why do **mypropBAD** and **mypropGOOD** work differently when the only difference is a $system(“”) call which does nothing? @(state[2], state[1], state[0]) (state!=3’b000) |-\> (b==1’b0, **$system(“”)** ); // difference in bold ---
**Author:** ![user49](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/user49/32/1084_2.png) [@user49](https://verificationacademy.com/forums/u/user49)\ **Post date:** [June 10, 2022, 4:53pm UTC](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/7 "2022-06-10T16:53:30Z")
_In reply to [John Canfield](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/6):_ > Why do mypropBAD and mypropGOOD work differently when the only difference is a $system(“”) call which does nothing? It is most likely a tool issue. The addition of a sequence\_match\_item should not make a difference. ---
**Author:** ![John\_Canfield](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/j/d78d45/32.png) [@John\_Canfield](https://verificationacademy.com/forums/u/John_Canfield)\ **Post date:** [June 13, 2022, 9:39pm UTC](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/8 "2022-06-13T21:39:48Z")
It looks like that is the correct answer, thanks. It is tool dependent: ```auto # mypropBAD passed at 1000 # mypropGOOD passed at 1000 # mypropGOOD passed at 2000 # mypropGOOD passed at 3000 # mypropGOOD passed at 4000 # Info: RUNTIME_0068 testbench.sv (11): $finish called. # Time: 5 us, Iteration: 0, Instance: /top, Process: @INITIAL#5_0@. # stopped at time: 5 us ``` ```auto mypropGOOD passed at 1000 mypropBAD passed at 1000 mypropGOOD passed at 2000 mypropGOOD passed at 3000 mypropGOOD passed at 4000 Simulation complete via $finish(1) at time 5 US + 0 ``` ```auto # mypropGOOD passed at 1000 # mypropBAD passed at 1000 # mypropGOOD passed at 2000 # mypropBAD passed at 2000 # mypropGOOD passed at 3000 # mypropBAD passed at 3000 # mypropGOOD passed at 4000 # mypropBAD passed at 4000 # ** Note: $finish : testbench.sv(11) # Time: 5 us Iteration: 0 Instance: /top ``` ```auto mypropBAD passed at 0 mypropGOOD passed at 0 mypropBAD passed at 1000 mypropGOOD passed at 1000 mypropBAD passed at 2000 mypropGOOD passed at 2000 mypropBAD passed at 3000 mypropGOOD passed at 3000 mypropBAD passed at 4000 mypropGOOD passed at 4000 $finish called from file "testbench.sv", line 11. $finish at simulation time 5000 ``` ---
**Author:** ![user49](https://verificationacademy.com/forums/user_avatar/verificationacademy.com/user49/32/1084_2.png) [@user49](https://verificationacademy.com/forums/u/user49)\ **Post date:** [June 13, 2022, 9:55pm UTC](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/9 "2022-06-13T21:55:00Z")
_In reply to [John Canfield](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/8):_ Thanks for the info. Please note that we DO NOT DISCUSS TOOLS in this forum. If there is a tool issue, avoid naming the tool; you can talk about the malfunction in a more generic manner, like “it worked with tool A, but failed with tool B”. The purpose of this forum is to address language usages, understandings, approaches to technical requirements, solutions, etc… EDA playground is neat, but IMHO, if we start talking about vendors’ issues we may lose the access. ---
**Author:** ![John\_Canfield](https://verificationacademy.com/forums/letter_avatar_proxy/v4/letter/j/d78d45/32.png) [@John\_Canfield](https://verificationacademy.com/forums/u/John_Canfield)\ **Post date:** [June 13, 2022, 11:46pm UTC](https://verificationacademy.com/forums/t/assertion-failing-to-check-all-cases/40509/10 "2022-06-13T23:46:29Z")
Okay, understood and sorry about that. I just thought it might be helpful info for others who run into the issue, but I understand and have edited my posts as you suggest. Thanks.