Verification of systems containing counters
- 1 January 1992
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
It is pointed out that systems containing counters have very large and deep state spaces, and the verification of properties on these systems can be very expensive in terms of memory space and computation time. A technique for automatically reducing the state space associated with the system on which some properties that can express both safeness and fairness constraints have to be proved is presented. In particular, a set of conditions upon which some counters can be reduced to three-state, nondeterministic machines is given. The controllers can be simplified by removing the redundancy induced by their interaction with the counter, so that the verification tasks can be more easily performed.Keywords
This publication has 5 references indexed in Scilit:
- Design verification and reachability analysis using algebraic manipulationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- ATPG aspects of FSM verificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Sequential circuit verification using symbolic model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Model checking and abstractionPublished by Association for Computing Machinery (ACM) ,1992
- Software for Analytical Development of Communications ProtocolsAT&T Technical Journal, 1990