caa a22 4500 475797647 CHVBK 20180406123729.0 cr unu---uuuuu 170329e20001001xx s 000 0 eng 10.1023/A:1008748802907 doi (NATIONALLICENCE)springer-10.1023/A:1008748802907 Verification of Similar FSMs by Mixing Incremental Re-encoding, Reachability Analysis, and Combinational Checks [Elektronische Daten] [Stefano Quer, Gianpiero Cabodi, Paolo Camurati, Luciano Lavagno, Ellen Sentovich, Robert Brayton] 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. Kluwer Academic Publishers, 2000 BDDs nationallicence FSMs nationallicence reachability analysis nationallicence re-encoding nationallicence formal verification nationallicence Quer Stefano Dip. di Automatica e Informatica, Politecnico di Torino, Turin, Italy aut Cabodi Gianpiero Dip. di Automatica e Informatica, Politecnico di Torino, Turin, Italy aut Camurati Paolo Dip. di Automatica e Informatica, Politecnico di Torino, Turin, Italy aut Lavagno Luciano Dip. di Elettronica, Politecnico di Torino, Turin, Italy aut Sentovich Ellen Cadence Labs, Berkeley, CA, USA aut Brayton Robert Department of EECS, UCB, Berkeley, CA, USA aut Formal Methods in System Design Kluwer Academic Publishers 17/2(2000-10-01), 107-134 0925-9856 17:2<107 2000 17 10703 https://doi.org/10.1023/A:1008748802907 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008748802907 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Quer Stefano Dip. di Automatica e Informatica, Politecnico di Torino, Turin, Italy aut NATIONALLICENCE 700 1- Cabodi Gianpiero Dip. di Automatica e Informatica, Politecnico di Torino, Turin, Italy aut NATIONALLICENCE 700 1- Camurati Paolo Dip. di Automatica e Informatica, Politecnico di Torino, Turin, Italy aut NATIONALLICENCE 700 1- Lavagno Luciano Dip. di Elettronica, Politecnico di Torino, Turin, Italy aut NATIONALLICENCE 700 1- Sentovich Ellen Cadence Labs, Berkeley, CA, USA aut NATIONALLICENCE 700 1- Brayton Robert Department of EECS, UCB, Berkeley, CA, USA aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 17/2(2000-10-01), 107-134 0925-9856 17:2<107 2000 17 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer