| 摘要 |
PURPOSE: To provide the method which checks the propriety of a finite state sequential machine at a high speed without requiring a large memory capacity. CONSTITUTION: The method which calculates an inverted image of a transition function Δ(δ, δ') of a product finite state machine(PFSM) consists of a step (a) where Δ-1 (En-1 ) obtained from a set of (n-1) equivalent states is called (a) section and BDD of a graph of a global function from S to S indicated by C(En-1 ) is canonically generated from BDD of a graph of an equivalent function En-1 , a step (b) where a new vector δ<n-1> =C(En-1 )oδ is generated from the section and a vector δ, and a step (c) where a pair of equivalent states related to the vector δ<n-1> are calculated so as to have a pair of formulas. |
