Establishing latch correspondence for sequential circuits using distinguishing signatures

Janett Mohnke, Paul Molitor, Sharad Malik

Research output: Contribution to journalArticle

6 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)
Pages (from-to)33-46
Number of pages14
JournalIntegration, the VLSI Journal
Volume27
Issue number1
DOIs
StatePublished - Jan 1 1999

All Science Journal Classification (ASJC) codes

  • Software
  • Hardware and Architecture
  • 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