Method for using complete-1-distinguishability for FSM equivalence checking
US6035109A · kind A · utility
Assignee
Inventors
Key dates
| Filing date | Apr 22, 1997 |
| Grant date | Mar 7, 2000 |
| Priority date | — |
| Expiry date | Apr 22, 2017 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
The Complete-1-Distinguishability (C-1-D) property is used for simplifying FSM verification. This property eliminates the need for a traversal of the product machine for the implementation machine and the specification machine. Instead, a much simpler check suffices. This check consists of first obtaining a 1-equivalence mapping between the 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. 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, the synthesis/verification methodology provides another point in the tradeoff curve between constraints-on-synthesis versus complexity-of-verification.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.