Using complete-1-distinguishability for FSM equivalence checking

Pranav Ashar, Aarti Gupta, Sharad Malik

Research output: Contribution to journalArticle

3 Scopus citations

Abstract

This article introduces the notion of a Complete-1-Distinguishability (C-1-D) property for simplifying equivalence checking of finite state machines (FSMs). When a specification machine has the C-1-D property, the traversal of the product machine can be eliminated. Instead, a much simpler check suffices. The check consists of first obtaining a 1-equivalence mapping between the individually reachable states of the specification and the implementation machines, and then checking that it is a bisimulation relation. The C-1-D property can be used directly for specification machines on which it naturally holds - a condition that has not been exploited thus far in FSM verification. We also show how this property can be enforced on an arbitrary FSM by exposing some of its latch outputs as pseudo-primary outputs during synthesis and verification. In this sense, our synthesis/verification methodology provides another point in the trade-off curve between constraints-on-synthesis versus complexity-of-verification. Practical experiences with this methodology have resulted in success with several examples for which it is not possible to complete verification using existing implicit state space traversal techniques.

Original languageEnglish (US)
Pages (from-to)569-590
Number of pages22
JournalACM Transactions on Design Automation of Electronic Systems
Volume6
Issue number4
DOIs
StatePublished - Jan 1 2001

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

Keywords

  • Algorithms
  • Bisimulation relation
  • Complete-1-distinguishability
  • Equivalence checking
  • Finite state machine equivalence
  • Sequential logic synthesis
  • Theory
  • Verification

Fingerprint Dive into the research topics of 'Using complete-1-distinguishability for FSM equivalence checking'. Together they form a unique fingerprint.

  • Cite this