Checkers - SVA: The Power of Assertions in SystemVerilog - page 212

The checker verify_consistency verifies that the abstract FSM is an abstrac-
tion of the concrete one:

checker verify_consistency(state, astate, ...,
event clk = $inferred_clock,
untyped rst = $inferred_disable);
default clocking @clk; endclocking
default disable iff rst;

aidle: assert property (astate == AIDLE <-> state inside {IDLE1
, IDLE2})
else $error("Idle states inconsistent");
...
endchecker : verify_consistency

The checker verify_abstract_fsm verifies the behavior correctness of the
abstract FSM:

checker verify_abstract_fsm(astate, ...,
event clk = $inferred_clock,
untyped rst = $inferred_disable);
default clocking @clk; endclocking
default disable iff rst;

never_stuck: assert property ( s_eventually astate != AIDLE)
else $error("FSM stuck");
unexpected: assert property (astate != AERR)
else $error("Unexpected behavior detected");
...
endchecker : verify_abstract_fsm

Finally the top-level checker is as follows:

checker verify_fsm(state, ....,
event clk = $inferred_clock,
untyped rst = $inferred_disable);
default clocking @clk; endclocking
default disable iff rst;

astate_t astate;

abstract_fsm afsm(..., astate);
verify_consistency vcons(state, astate, ...);
verify_abstract_fsm vafsm(astate, ...);
endchecker : verify_fsm

Here state is the concrete state generated by the RTL. The ellipses ( ... ) des-
ignate other arguments that should be filled in, and are not part of the syntax. Note,
that we do not have to explicitly pass the clock and reset to the subcheckers because
they may be inferred by default via $inferred_clock and $inferred_disable
system functions.

t