About concurrent assertion in FSM

SystemVerilog
,
1

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)

2

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.

3

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

  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
4

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