About concurrent assertion in FSM

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