State space exploration of finite state machines is used to prove properties. 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 can be achieved through state minimization, partitioning, and re-encoding the FSMs to factor out their differences. This paper focuses on re-encoding presenting an incremental approach to re-encoding for sequential verification. Experimental results demonstrate the effectiveness of this solution on medium-large circuits where other techniques may fail.
Incremental re-encoding for symbolic traversal of product machines / Quer, Stefano; Lavagno, Luciano; Cabodi, Gianpiero; Sentovich, Ellen; Camurati, Paolo Enrico; Brayton, R. K.. - STAMPA. - (1996), pp. 158-163. (Intervento presentato al convegno Proceedings of the 1996 European Design Automation Conference with EURO-VHDL'96 and Exhibition tenutosi a Geneva (Switz.) nel 16-20 September 1996).
Incremental re-encoding for symbolic traversal of product machines
Quer Stefano;Lavagno Luciano;Cabodi Gianpiero;Camurati Paolo;
1996
Abstract
State space exploration of finite state machines is used to prove properties. 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 can be achieved through state minimization, partitioning, and re-encoding the FSMs to factor out their differences. This paper focuses on re-encoding presenting an incremental approach to re-encoding for sequential verification. Experimental results demonstrate the effectiveness of this solution on medium-large circuits where other techniques may fail.File | Dimensione | Formato | |
---|---|---|---|
eurodac1996.pdf
accesso aperto
Tipologia:
2. Post-print / Author's Accepted Manuscript
Licenza:
Pubblico - Tutti i diritti riservati
Dimensione
340.42 kB
Formato
Adobe PDF
|
340.42 kB | Adobe PDF | Visualizza/Apri |
Incremental_re-encoding_for_symbolic_traversal_of_product_machines.pdf
accesso riservato
Tipologia:
2a Post-print versione editoriale / Version of Record
Licenza:
Non Pubblico - Accesso privato/ristretto
Dimensione
631.38 kB
Formato
Adobe PDF
|
631.38 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11583/2981107