State space exploration of finite state machines is used to prove properties about sequential behavior, such as the equivalence of two machines. The three paradigms for exploring reachable states, forward traversal, backward traversal and a combination of the two, reach their limits on large practical examples. Approximate techniques and combinational verification are far less expensive but these imply sufficient, not strictly necessary conditions. Extending the applicability of the purely combinational check to pairs of machines with different encodings can be achieved through state minimization, partitioning, and re-encoding the FSMs to factor out their differences. This paper focuses on re-encoding: we present an incremental approach to re-encoding for sequential verification. We transform the product machine traversal to a combinational verification in the best case, and to a computationally simpler product machine traversal in the general case. Experimental results demonstrating the effectiveness of these techniques o medium-large circuits where other techniques may fail.

Incremental FSM Re-encoding for Simplifying Verification by Symbolic Traversal / Quer, Stefano; Cabodi, Gianpiero; Camurati, Paolo Enrico; Lavagno, Luciano; Sentovich, E. M.; Brayton, R. K.. - STAMPA. - (1995), pp. 317-327. (Intervento presentato al convegno ACM/IEEE International Workshop on Logic Synthesis (IWLS 1995) tenutosi a Lake Tahoe, California, USA nel May 1995).

Incremental FSM Re-encoding for Simplifying Verification by Symbolic Traversal

QUER, Stefano;CABODI, Gianpiero;CAMURATI, Paolo Enrico;LAVAGNO, Luciano;
1995

Abstract

State space exploration of finite state machines is used to prove properties about sequential behavior, such as the equivalence of two machines. The three paradigms for exploring reachable states, forward traversal, backward traversal and a combination of the two, reach their limits on large practical examples. Approximate techniques and combinational verification are far less expensive but these imply sufficient, not strictly necessary conditions. Extending the applicability of the purely combinational check to pairs of machines with different encodings can be achieved through state minimization, partitioning, and re-encoding the FSMs to factor out their differences. This paper focuses on re-encoding: we present an incremental approach to re-encoding for sequential verification. We transform the product machine traversal to a combinational verification in the best case, and to a computationally simpler product machine traversal in the general case. Experimental results demonstrating the effectiveness of these techniques o medium-large circuits where other techniques may fail.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2654246
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo