| 摘要 |
PURPOSE: A method and a device for repeatedly computing an over-approximate reachable state are provided to redivide a circuit to a direction favorable to the approximation performance improvement by compressing a state transition function BDD(Binary Decision Diagram) with the use of the state transition corresponding to a "don't care" condition based on a previous analysis result of each analysis. CONSTITUTION: A "don't care" BDD is generated by extracting an unreachable state from a present state transition relation BDD(1). The present state transition function BDD is compressed by using the "don't care" BDD(5). A new state transition relation BDD is generated by using the compressed state transition function BDD, and the new state transition relation BDD is compressed again by using the "don't care" BDD(6). The previous step is repeated if the improvement of the approximation exists by judging that the quality improvement of the over-approximation according to the compression of the new state transition relation BDD. If not, the approximation is concluded as a final result.
|
