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 language | English (US) |
---|---|
Pages (from-to) | 346-353 |
Number of pages | 8 |
Journal | IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers |
State | Published - Dec 1 1996 |
Externally published | Yes |
Event | Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design - San Jose, CA, USA Duration: Nov 10 1996 → Nov 14 1996 |
All Science Journal Classification (ASJC) codes
- Software
- Computer Science Applications
- Computer Graphics and Computer-Aided Design