Chipress

Jasper Gold offers “fsm_checks” command to auto-generate properties for FSM state / transition reachability. When running this command, the tool automatically detects FSM state variables or accepts user-specified FSM state variables, and extracts cover properties to prove.

To define a conceptual FSM from the the concatenation of “signal0” and “signal1“:

# The outermost brace bracket defines the FSM spec, which consists of FSM signals and a list of FSM states
# The list of FSM states is an alternating list of values and labels
fsm_checks -add_fsm {{{signal0, signal1}} {0 `IDLE 1 `WRITE 2 `READ 3 `WAIT}}

To generate properties for state reachability for both user-defined and automatically identified FSMs:

fsm_checks -states

To generate properties for state transition reachability for both user-defined and automatically identified FSMs:

fsm_checks -trans

To generate dead end properties for both user-defined and automatically identified FSMs:

fsm_checks -deadend

To generate state checks between FSMs:

# This command creates a new task for each pair of FSMs
fsm_checks -cross