About concurrent assertion in FSM

[GIREESHNP]

Hi guys
am getting the syntax error at non overlapped operator which is shown below, can you people plz check and tell me as soon as possible
am writing assertion for FSM to verify the states

property peak; @(posedge clk) ( {(present_state == state0) && ( in |=> present_state == stste1 ), abort(!rst) });

a:assert property(peak)

[warnerrs]

Implication operators can only be used inside property expressions. Where you’re using it, it is inside a sequence expression, hence the syntax error.

Can’t help you rewrite that though, as you didn’t describe what the property is supposed to do, and I can’t make it out from your code.

[ben2]

In reply to warnerrs:

• You don’t need to write a separate property if the assertion does not have arguments or if the assertion does not use local variables.
• Use the default clocking @(posedge clk); endclocking instead of defining the clock in every assertion.
• On signal notations, I like the _n for active low variables

ap: assert property(@ (posedge clk) // not needed if using default clocking 
  disable iff ($sampled(!rst_n)) // glitch free disable using the $sampled function 
    (present_state == state0) && in |=> present_state == state1);  
// disable iff (!rst_n) // async disable  
 

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

---

1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
3. “Using SVA for scoreboarding and TB designs”
   http://systemverilog.us/papers/sva4scoreboarding.pdf
4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
   October 2013 | Volume 9, Issue 3 | Verification Academy
5. SVA in a UVM Class-based Environment
   SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

[ben2]

In reply to ben@SystemVerilog.us:

Keep in mind that an assertion of that type is similar to an enabled FF.
More interesting assertions address the requirements of the design.
Ben systemverilog.us