Using Complete-1-Distinguishability for FSM equivalence checking

Pranav Ashar, Aarti Gupta, Sharad Malik

Research output: Contribution to journalConference article

9 Scopus citations

Abstract

This paper introduces the use of the Complete-1-Distinguishability (C-1-D) property for simplifying FSM verification. This property eliminates the need for a traversal of the product machine for the implementation and the specification. Instead, a much simpler check suffices. This check consists of first obtaining a 1-equivalence mapping between states of the two machines, and then checking that it is a bisimulation relation. The C-1-D property can be used directly on specifications for 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 arbitrary FSMs by exposing some of the latch outputs as pseudo-primary outputs during synthesis and verification. In this sense, our synthesis/verification methodology provides another point in the tradeoff curve between constraints-on-synthesis versus complexity-of-verification. Practical experiences with using 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)346-353
Number of pages8
JournalIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers
StatePublished - Dec 1 1996
Externally publishedYes
EventProceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design - San Jose, CA, USA
Duration: Nov 10 1996Nov 14 1996

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design

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

Cite this