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

level modules through their input ports and is obtained from them through their
output ports. Therefore output ports are a key feature in enabling design modularity.
The same is true for the verification IP: splitting a checker into smaller checkers is
made possible using checker output arguments.
Complex checkers are typical in formal verification when they contain a sophis-
ticated modeling and numerous assertions. To make such checker manageable, it
should be split into smaller parts, each part containing either modeling of some
block or assertions and assumptions imposed to this block.

Example 9.31. Suppose that we want to verify an FSM implemented in RTL. This
FSM may be rather complex, have many states, sophisticated logic required to make
this FSM efficient, etc. The complexity of this FSM may prevent its direct formal
verification. For the purpose of verification we may not need to account for all
its complexity. We can build a model of a more abstract FSM that may be easily
verified. For example, the concrete FSM may have two different idle states: IDLE1
and IDLE2 . This fact may be irrelevant for formal verification, hence our abstract
FSM has a single idle state AIDLE . Transitions of the abstract FSM may also be
much simpler than those of the concrete FSM, because irrelevant implementation
details may be ignored.
The checker verifying the concrete FSM may be split into the following parts:

￿ Abstract FSM model

￿ Assertions verifying that the behavior of the abstract FSM is aligned to the

behavior of the concrete one

￿ Assertions verifying the behavior of the abstract FSM (and therefore, the relevant

behavior of the concrete one)

￿ Glue that combines all the above parts together

Let enumeration types state_t and astate_t contain definitions of the concrete
and abstract states, respectively:

typedef enum {IDLE1 = ..., IDLE2 = ..., ...} state_t;
typedef enum {AIDLE, ..., AERR} astate_t;

The checker implementing the abstract FSM will look like that:

checker abstract_fsm(...,
event clk = $inferred_clock,
untyped rst = $inferred_disable,
output astate_t astate); // abstract state
default clocking @clk; endclocking
always_ff @clk begin
if (rst) astate <= AIDLE;
case (astate)
AIDLE: astate <= ...;
...
default : astate <= AERR;
endcase
end
endchecker : abstract_fsm