The reach command computes the reachability of states for a given signal. Reachability is defined as a transition path from an initial state to a given state. The reach command It also performs deadlock checking on all reachable states. Deadlock is a situation where a transition path into a state exists, but no transition state out of a state exists. For example, given the following code which is intended to be a modulo-5 counter:

 reg [3:0] cnt;
 always @(posedge clk)
   if (cnt > 5)

      cnt <= 0;

   else if (cnt < 5)
      cnt <= cnt + 1;

Produces the following reach output:

> init cnt 0
     Signal 'cnt' initialized to 0b0

> reach -detail cnt

---------------------- cnt ----------------------
   State '0000': Initial state
   State '0001': Reachable
   State '0010': Reachable
   State '0011': Reachable
   State '0100': Reachable
   State '0101': Reachable - Dead
   State '0110': Not reachable
   State '0111': Not reachable
   State '1000': Not reachable
   State '1001': Not reachable
   State '1010': Not reachable
   State '1011': Not reachable
   State '1100': Not reachable
   State '1101': Not reachable
   State '1110': Not reachable
   State '1111': Not reachable

   Total States : 16
   Reachable States : 6
   Unreachable States: 10
   Dead States : 1
   

States 0 through 5 are reachable, but state 5 is a dead state. Once it is entered, it cannot be exited. Additionally, states 6 through 15 are not reachable from the initial state.

To perform reachability analysis on a signal, select the signal's parent component in the Components Window then select the desired signal in the Signals Window. Then, use the Analyze menu (Analyze->Reach...) to invoke the Reach Options dialog.

Max: Maximum number of algorithm iterations to perform. Large vectors can require the reach algorithm to perform huge numbers of computational iterations. This control will set an upper limit to avoid having the application hang for long periods of time.

Restrict: If the signal to be analyzed has large input vectors driving it, the state space can become needlessly large. This control will automatically restrict to 0 those inputs whose width is greater than the value set, effectively removing them from the state space. Any user defined restrictions will not be overridden. A value of 0 for restrict will prevent any signals from being auto-restricted.

Include details in output: Selecting this check box will enable detailed output from the analysis. Detailed output includes information for each state analyzed including whether it's reachable or not and whether it is a dead state. The default output is a summary of the number of states tested, how many were reachable and how many were dead.

States: Sometimes it is not desirable to test all possible states of a signal. One example would be a one-hot encoded state-machine state register. For these cases, the specific states to be analyzed can be enumerated in this entry box. The desired states may include individual states expressed in binary (i.e. 0b10100), decimal, or hexadecimal (i.e. 0xfefe) formats, the keywords '1hot' (for one-hot encoded states, i.e. 0001, 0010, 0100, 1000), '0hot' (for zero-hot encoded states, i.e. 1110, 1101, 1011, 0111) or ranges (i.e. 0x100-0x200). The default is to analyze all states.

 

Limitations

Performing reachability analysis on large vectors can be very time consuming. Typically, you'll want to perform checking on vectors less than 16 bits. Since state-machine vectors are rarely larger than 16 bits (except for one-hot encoded vectors), this limitation should not be too restrictive.

 

reach Command

Reachability analysis can also be run using the reach command entered in the GUI Command Entry box or on the command line in command-line mode. The reach command format is:

SYNTAX
       (void) reach
            [-detail]
            [-max <#>
            [-states <list>]
            <signal>

ARGUMENTS
 -detail
   Include details about each state's reachabil­
   ity/deadlock in output. Default is to produce a
   summary only.

 -max <#>
   Maximum number of algorithm iterations to perform.
   Large vectors can require the reach algorithm to
   perform huge numbers of computation iterations.
   -max will set an upper limit to avoid having the
   application hang for long periods of time. The
   default value is 10000.

 -restrict <#>
   If the signal to be analyzed has large  input  vec­
   tors  driving  it, the state space can become need­
   lessly large. -restrict will automatically restrict
   inputs whose width is greater than <#> to 0, effec­
   tively removing them from the state space. Any user
   defined  restrictions  on  <expression> will not be
   overridden. A value of 0 for <#> will  prevent  any
   signals from being auto-restricted. The default for
   -restrict is 0.

 -states <list>
   List of states to be checked. <list> must be a
   comma separated list of state values and may
   include individual states expressed in binary (i.e.
   0b10100), decimal, or hexadecimal (i.e. 0xfefe)
   formats, the keywords '1hot' (for one-hot encoded
   states, i.e. 0001, 0010, 0100, 1000), '0hot' (for
   zero-hot encoded states, i.e. 1110, 1101, 1011,
   0111) or ranges (i.e. 0x100-0x200). Default is to
   check all states.

 <signal>
   Signal name on which to perform reachability/dead­
   lock checking.