Establishing latch correspondence for sequential circuits using distinguishing signatures

Janett Mohnke, Paul Molitor, Sharad Malik

Research output: Contribution to conferencePaperpeer-review

1 Scopus citations

Abstract

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.

Original languageEnglish (US)
Pages472-476
Number of pages5
StatePublished - Dec 1 1997
EventProceedings of the 1997 40th Midwest Symposium on Circuits and Systems. Part 1 (of 2) - Sacramento, CA, USA
Duration: Aug 3 1997Aug 6 1997

Other

OtherProceedings of the 1997 40th Midwest Symposium on Circuits and Systems. Part 1 (of 2)
CitySacramento, CA, USA
Period8/3/978/6/97

All Science Journal Classification (ASJC) codes

  • Electronic, Optical and Magnetic Materials
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Establishing latch correspondence for sequential circuits using distinguishing signatures'. Together they form a unique fingerprint.

Cite this