TY - CONF
T1 - Establishing latch correspondence for sequential circuits using distinguishing signatures
AU - Mohnke, Janett
AU - Molitor, Paul
AU - Malik, Sharad
N1 - Funding Information:
Janett Mohnke received her M.S. degree in computer science from Humboldt University at Berlin, Germany, in 1991. From 1991 to 1994, she worked within the Sonderforschungsbereich “VLSI Design Methods and Parallelism” at University of Saarland, Germany, and at Humboldt University. From June to November 1992, she visited Princeton University under a grant from IREX. From 1995 to 1997, Janett Mohnke worked at Martin-Luther-University in Halle, Germany, where she is currently finishing her Phd. Since May 1997, she has been working with the company DResearch Digital Media Systems GmbH in Berlin, Germany. Her research interests include the logic synthesis and verification of digital circuits.
PY - 1997
Y1 - 1997
N2 - This paper addresses the problem of establishing the unknown correspondence for the latch variables of two sequential circuits which have the same state encoding. This has direct application in finite state machine verification: If a one-to-one correspondence can be established between the latches of two circuits, then checking for their equivalence reduces to a much simpler combinational equivalence check problem. The approach presented in this paper is based on methods used to solve the unknown correspondence problem for inputs and outputs in combinational circuits. It computes input and novel latch output signatures, using ROBDDs, for each latch variable of a circuit that help to establish correspondence. Experimental results on a large set of benchmarks show the efficacy of this approach.
AB - This paper addresses the problem of establishing the unknown correspondence for the latch variables of two sequential circuits which have the same state encoding. This has direct application in finite state machine verification: If a one-to-one correspondence can be established between the latches of two circuits, then checking for their equivalence reduces to a much simpler combinational equivalence check problem. The approach presented in this paper is based on methods used to solve the unknown correspondence problem for inputs and outputs in combinational circuits. It computes input and novel latch output signatures, using ROBDDs, for each latch variable of a circuit that help to establish correspondence. Experimental results on a large set of benchmarks show the efficacy of this approach.
UR - http://www.scopus.com/inward/record.url?scp=0031376592&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0031376592&partnerID=8YFLogxK
M3 - Paper
AN - SCOPUS:0031376592
SP - 472
EP - 476
T2 - Proceedings of the 1997 40th Midwest Symposium on Circuits and Systems. Part 1 (of 2)
Y2 - 3 August 1997 through 6 August 1997
ER -