Temporal Proofs are a method of testing state transitions for correct operation. A series of Temporal Proofs can be performed on sequenial logic to verify its correct functionality, all without the need to write a testbench.

Temporal Proofs are an extension of reachability analysis in that paths between states transitions can be analyzed. For example, using Temporal Proofs it is easy to determine if the initial state can be reached from every other state.

Temporal Proofs are specified using logic expressions with temporal operators based on Computation Tree Logic (CTL). X-Amin contains 10 CTL operators:

• EX(A): Next state after condition A is true along some state-sequence path
• AX(A): Next state after condition A is true along all state-sequence paths
• EF(A): Some state in the future after condition A is true along some state-sequence path
• AF(A): Some state in the future after condition A is true along all state-sequence paths
• EG(A): All states in the future after condition A is true along some state-sequence path
• AG(A): All states in the future after condition A is true along all state-sequence paths
• EU(A, B): Along some state-sequence path, condition A is true until condition B is true
• AU(A, B): Along all state-sequence paths, condition A is true until condition B is true
• ER(A, B): Along some state-sequence path, condition B is true until condition A releases B
• AR(A, B): Along all state-sequence paths, condition B is true until condition A releases B
  

Example: A simple mod 4 counter.

 reg [1:0] cnt;
 always @(posedge clk)
    cnt <= cnt + 1;
  

Prove that the next value of cnt is 1 when cnt starts at 0. Also prove that the next value is not 2, but will become 2 at some future time.

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

> prove cnt EX(cnt==1)
The rule is true

> prove cnt EX(cnt==2)
The rule is false

> prove cnt EF(cnt==2)
The rule is true

CTL operators can also be nested. The following example can be used to prove that the initial state can always be reached from all execution paths:

> prove cnt AG(EF(cnt==0))

The rule is true

To perform a Temporal Proof from GUI mode, select the desired component in the Components Window then select the desired signal in the Signals Window. Note that the signal must be a clocked signal in order to run Temporal Proofs. Then, use the Analyze menu (Analyze->Prove) or the Prove icon on the Analyze toolbar to invoke the Prove dialog.

Simply fill in the expression to be proven.

 

Limitations

Performing temporal 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.

 

prove Command

Temporal proofs can also be run using the prove command entered in the GUI Command Entry box or on the command line in command-line mode. The prove command format is:

SYNTAX
       (void) prove
            [-max <#>]
            <sig>
            <expression>

ARGUMENTS
 -max <#>
   Maximum number of algorithm iterations to perform.
   Large vectors can require the temporal operator
   algorithms 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..TP <sig> Signal
   name on which to perform the temporal analysis


<sig>
   Signal to be analyzed

 <expression>
   Temporal expression to be analyzed