US6035109A
Expired / Lapsed
US
⏱️ 0.0 years remaining
Method for using complete-1-distinguishability for FSM equivalence checking
Assignee: NEC Corp
•
Filing: 1997-04-22
•
Granted: 2000-03-07
•
Expires: 2017-04-22
Abstract
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.
Inventors
- 👤 Pranav N Ashar
- 👤 Aarti Gupta
- 👤 Sharad Malik
Bibliographic Details
Application Number
—
Jurisdiction
US
Data Source
google_patents
Last Synchronized
2026-11-06 22:28
CPC Classifications
G; G06; G06F; G06F30/00; G06F30/30; G06F30/32; G06F30/33; G06F30/3323
Claims Analysis
Total Claims: 11
Claim 1
Independent Claim
169 words
A method for determining the equivalence of a specification finite state machine M1, having a Complete-1-Distinguishability property wherein all state pairs are 1-distinguishable such that each state of the specification finite state machine M1 can be distinguished from all other states by an input sequence of length 1, to an implementation finite state machine M2, the method including: performing a traversal on the specification finite state machine M1 to obtain a set of all reachable states; determining if the specification finite state machine M1 has the Complete-1-Distinguishability property on all reachable states; performing sequential synthesis to obtain the implementation finite state machine M2; performing a traversal on the implementation finite state machine M2 to obtain a set of all reachable states; performing a 1-equivalence mapping between reachable states of the specification finite state machine M1 and the implementation finite state machine M2; and determining if the 1-equivalence mapping is a bisimulation relation, thereby indicating that the specification finite state machine M1 and implementation finite state machine M2 are equivalent.
Claim 2
Independent Claim
169 words
A method for determining the equivalence of a specification finite state machine M1, having a Complete-1-Distinguishability property wherein all state pairs are 1-distinguishable such that each state of the specification finite state machine M1 can be distinguished from all other states by an input sequence of length 1, to an implementation finite state machine M2, the method including: performing a traversal on the specification finite state machine M1 to obtain a set of all reachable states; determining if the specification finite state machine M1 has the Complete-1-Distinguishability property on all reachable states; performing sequential synthesis to obtain the implementation finite state machine M2; performing a traversal on the implementation finite state machine M2 to obtain a set of all reachable states; performing a 1-equivalence mapping between reachable states of the specification finite state machine M1 and the implementation finite state machine M2; and determining if the 1-equivalence mapping is a bisimulation relation, thereby indicating that the specification finite state machine M1 and implementation finite state machine M2 are equivalent.
Claim 3
Dependent Claim
146 words
The method as claimed in claim 1, wherein the step of 1-equivalence mapping defines a relation χ between the reachable states of the specification finite state machine M1 and implementation finite state machine M2, as follows, ##EQU8## wherein .OR right. means is a subset of, P,Q are the sets of states of the specification finite state machine M1 and the implementation finite state machine M2, p,q are states of the specification finite state machine M1 and the implementation finite state machine M2, x means a cross product of, { } means a set, | means such that, and χ means the 1-equivalance mapping between the reachable states of the specification finite state machine M1 and the implementation finite state machine M2; wherein χ captures those pairs of reachable states between the specification finite state machine M1 and the implementation finite state machine M2 that are 1-equivalent.
Claim 4
Dependent Claim
21 words
The method as claimed in claim 2, the step of 1-equivalence mapping further includes ensuring relation χ is a one-to-many mapping.
Claim 5
Dependent Claim
42 words
The method as claimed in claim 1, wherein the step of performing a transversal on the specification finite state machine M1 further includes assuming that all states in the specification finite state machine M1 are reachable if the transversal does not complete.
Claim 6
Dependent Claim
40 words
The method as claimed in claim 1, wherein a subset of latches on the specification finite state machine M1 are exposed as pseudo-primary outputs to enforce the Complete-1-Distinguishability property if specification finite state machine M1 fails the Complete-1-Distinguishability property determination.
Claim 7
Dependent Claim
70 words
The method as claimed in claim 5, wherein the step of exposing a subset of latches on the specification finite state machine M1 as pseudo-primary outputs further includes: obtaining a set of all distinct state pairs which need to be distinguished; identifying the latches that exhibit a different value in at least one of the distinct state pairs, and selecting a subset of latches which cover all distinct state pairs.
Claim 8
Dependent Claim
45 words
The method as claimed in claim 6, wherein the step of exposing a subset of latches on the specification finite state machine M1 as pseudo-primary outputs further includes the removal of any logic/wiring associated with the pseudo-primary outputs in the implementation finite state machine M2.
Claim 9
Dependent Claim
42 words
The method as claimed in claim 1, wherein the step of performing a transversal on the implementation finite state machine M2 further includes assuming that all states in the implementation finite state machine M2 are reachable if the transversal does not complete.
Claim 10
Dependent Claim
335 words
The method as claimed in claim 1, wherein the determination of whether the 1-equivalence mapping is a bisimulation relation further includes: ##EQU9## wherein ∀ means for all, i is an input, ε means is an element of, I is a set of inputs, p and s are states of the specification finite state machine M1 having a transition i therebetween, q and t are states of the implementation finite state machine M2 having a transition i therebetween, Δ 1 and Δ 2 are the transition relations of the specification finite state machine M1 and the implementation finite state machine M2, respectively, means then, ∃ means there exists, P and Q are sets of states of the specification finite state machine M1 and the implementation finite state machine M2, respectively, means and, χ means the 1-equivalence mapping between the reachable states of the specification finite state machine M1 and the implementation finite state machine M2; and wherein equation (1) states that for all inputs i, which are an element of I, such that there is an i transition from state p to state s, which belongs to transition relation Δ 1 , then there exists a state t, which belongs to the set of states Q, such that there is an i transition from state q to state t, which belongs to transition relation Δ 2 , and wherein states s and t belong to χ; wherein equation (2) states that for all inputs i, which are an element of I, such that there is an i transition from state q to state t, which belongs to transition relation Δ 2 , then there exists a state s, which belongs to the set of states P, such that there is an i transition from state p to state s, which belongs to transition relation Δ 1 , and wherein states s and t belong to χ; and calculating equation (1) and equation (2) for every state pair where the states are 1-equivalent and are individually reachable.
Claim 11
Dependent Claim
57 words
The method as claimed in claim 9, wherein the step of determining whether the 1-equivalence mapping is a bisimulation relation further includes: determining if equation (1) equals equation (2) for all inputs i; and declaring specification finite state machine M1 equivalent to implementation finite state machine M2 if equation (1) equals equation (2) for all inputs i.
References Cited (Backward Citations)
USPTO Annuity & Maintenance Windows
| Annuity Stage | Window Opens | Payment Deadline | Surcharge Period Until | Estimated Fee | Status |
|---|---|---|---|---|---|
| 3.5 Years (Year 4) | 2003-03-07 | 2003-09-06 | 2004-03-07 | $2000.00 | Window Closed / Lapsed |
| 7.5 Years (Year 8) | 2007-03-07 | 2007-09-06 | 2008-03-07 | $3760.00 | Window Closed / Lapsed |
| 11.5 Years (Year 12) | 2011-03-07 | 2011-09-06 | 2012-03-07 | $7700.00 | Window Closed / Lapsed |