When performing Temporal Proofs and Reachability/Deadlock tests it is necessary to define an initial state for the signal being analyzed. If no state if defined, X-Amin automatically sets the initial state to zero. The init command is used to set a signal to other initial values.

To initialize a signal in GUI mode, select the signal's parent component in the Component Window then select the desired signal in the Signal Window. Use the Command menu (Command->Init...) or Signals Window popup menu (right mouse button->Init...) to invoke the Init Options dialog.

Value: Simply enter the initialization value. If the size of the value is greater than the signal can accomodate, the value will be truncated to the appropriate number of bits.

 

init Command

Signals can be also be initialized using the init command entered in the GUI Command Entry box or on the command line in command-line mode. The init command format is:

SYNTAX
 (void) init
   <sig>
   <value>
   

ARGUMENTS
 <sig> Signal name to initialize

 <value>
   Numeric value to initialize <sig> to.
   

Restricting

When performing logic analysis it is sometimes beneficial to restrict an input to a specific value to either perform a specific test of that signal value or to remove the effect of the signal from the rest of the combinational logic. For example, given the following HDL code:

 reg d;
 always @(posedge clk or posedge rst)
    if (!rst)
       d <= 0;
    else if (ld)
       d <= a & b;
  

The following truth table is obtained using the eval command:

> eval d
 d
 -----------------
 a b d ld rst | d 
 0 0 0 0   0  | 0 
 0 0 0 0   1  | 0 
 0 0 0 1   0  | 0 
 0 0 0 1   1  | 0 
 0 0 1 0   0  | 0 
 0 0 1 0   1  | 1 
 0 0 1 1   0  | 0 
 0 0 1 1   1  | 0 
 0 1 0 0   0  | 0 
 0 1 0 0   1  | 0 
 0 1 0 1   0  | 0 
 0 1 0 1   1  | 0 
 0 1 1 0   0  | 0 
 0 1 1 0   1  | 1 
 0 1 1 1   0  | 0 
 0 1 1 1   1  | 0 
 1 0 0 0   0  | 0 
 1 0 0 0   1  | 0 
 1 0 0 1   0  | 0 
 1 0 0 1   1  | 0 
 1 0 1 0   0  | 0 
 1 0 1 0   1  | 1 
 1 0 1 1   0  | 0 
 1 0 1 1   1  | 0 
 1 1 0 0   0  | 0 
 1 1 0 0   1  | 0 
 1 1 0 1   0  | 0 
 1 1 0 1   1  | 1 
 1 1 1 0   0  | 0 
 1 1 1 0   1  | 1 
 1 1 1 1   0  | 0 
 1 1 1 1   1  | 1 
 -----------------
   

If we are only concerned with the cases where rst = 1, we can restrict rst with the following eval results:

> restrict rst d 1
> eval d 
 d
 -------------
 a b d ld | d 
 0 0 0 0  | 0 
 0 0 0 1  | 0 
 0 0 1 0  | 1 
 0 0 1 1  | 0 
 0 1 0 0  | 0 
 0 1 0 1  | 0 
 0 1 1 0  | 1 
 0 1 1 1  | 0 
 1 0 0 0  | 0 
 1 0 0 1  | 0 
 1 0 1 0  | 1 
 1 0 1 1  | 0 
 1 1 0 0  | 0 
 1 1 0 1  | 1 
 1 1 1 0  | 1 
 1 1 1 1  | 1 
 -------------
  

Now, if we want to remove signal 'a' from the combinational network, we can restrict its value to 0 and obtain the following eval results:

> restrict a d 0
> eval d 
 d
 ---------
 d ld | d 
 0 0  | 0 
 0 1  | 0 
 1 0  | 1 
 1 1  | 0 
 ---------

Note that when a signal is restricted, the restriction only affects the target signal. In the above example, if the signal 'a' was contained in the combinational network for signal 'z', the previous restrictions on 'a' would not affect the analyzes of signal 'z'.

To restrict an input to a signal in GUI mode, select the signal's parent component in the Component Window then select the desired signal in the Signal Window. Use the Command menu (Command->Restrict...) or Signals Window popup menu (right mouse button->Restrict...) to invoke the Restrict Options dialog.