State space exploration is often used to prove properties about sequential behavior of Finite State Machines (FSMs). For example, equivalence of two machines is proved by analyzing the reachable state set of their product machine. Nevertheless, reachability analysis is infeasible on large practical examples. Combinational verification is far less expensive, but on the other hand its application is limited to combinational circuits, or particular design schemes. Finally, approximate techniques imply sufficient, not strictly necessary conditions. The purpose of this paper is to extend the applicability of purely combinational checks. This is generally achieved through state minimization, partitioning, and re-encoding the FSMs to factor out their differences. We focus on re-encoding. In particular, we present an incremental approach to re-encoding for verification that transforms the product machine traversal into a combinational verification in the best case, and into a computationally simpler product machine traversal in the general case. Experimental results demonstrate the effectiveness of this technique on medium-large circuits where other techniques may fail.

Verification of Similar FSMs by Mixing Incremental Re-encoding Reachability Analysis and Combinational Checks / Quer, Stefano; Cabodi, Gianpiero; Camurati, Paolo Enrico; Lavagno, Luciano; E. M., Sentovich; R. K., Brayton. - In: FORMAL METHODS IN SYSTEM DESIGN. - ISSN 0925-9856. - 17:2(2000), pp. 107-134. [10.1023/A:1008748802907]

Verification of Similar FSMs by Mixing Incremental Re-encoding Reachability Analysis and Combinational Checks

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

Abstract

State space exploration is often used to prove properties about sequential behavior of Finite State Machines (FSMs). For example, equivalence of two machines is proved by analyzing the reachable state set of their product machine. Nevertheless, reachability analysis is infeasible on large practical examples. Combinational verification is far less expensive, but on the other hand its application is limited to combinational circuits, or particular design schemes. Finally, approximate techniques imply sufficient, not strictly necessary conditions. The purpose of this paper is to extend the applicability of purely combinational checks. This is generally achieved through state minimization, partitioning, and re-encoding the FSMs to factor out their differences. We focus on re-encoding. In particular, we present an incremental approach to re-encoding for verification that transforms the product machine traversal into a combinational verification in the best case, and into a computationally simpler product machine traversal in the general case. Experimental results demonstrate the effectiveness of this technique on 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/1397886
 Attenzione

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