Formal Boolean manipulations for the verification of sequential machines
- 4 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The paper addresses the problem of verifying synchronous sequential machines. It first shows that there is a certain class of temporal properties that can be verified by proving two sequential machines equivalent. It then explains that the equivalence of two sequential machines can be checked without building any state diagram. It is sufficient to observe all the valid states of a machine, which can be done by traversing its state diagram. It finally presents the symbolic manipulation used to perform the traversal of a state diagram in a more efficient way than the usual traversal technique based on enumeration.Keywords
This publication has 3 references indexed in Scilit:
- On the verification of sequential machines at differing levels of abstractionIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1988
- Research on Automatic Verification of Finite-State Concurrent SystemsAnnual Review of Computer Science, 1987
- Fairness and related properties in transition systems ? a temporal logic to deal with fairnessActa Informatica, 1983