LIP6 1997/028
- Reports
Vérification compositionnelle de modèle basée sur une bisimulation dépendant de la propriété - F. Rahim, E. Encrenaz
- 20 pages - 11/12/1997- document en - http://www.lip6.fr/lip6/reports/1997/lip6.1997.028.ps.gz - 69 Ko
- Contact : Emmanuelle.Encrenaz (at) nulllip6.fr
- Ancien Thème : ANP
- Keywords : formal verification, equivalence relation, bisimulation, finite state machine (FSM), CTL, VHDL
- Publisher : Emmanuelle.Encrenaz (at) nulllip6.fr
Large designs are commonly modelled as a set of interconnected finite state machines (FSM). The basic approach to model checking such designs is to first build the product of the component FSMs and then traverse (e.g. symbolically) this single FSM. Even when using symbolic representations based on BDDs, we have to face the state explosion problem.
We present in this work a concept of state equivalence that is defined with respect to a given CTL formula. This equivalence is used to reduce the size of each component FSM so that their product will be smaller. Contrary of strong bisimulation, it does not preserve all CTL formulae, so we can expect to compute coarser equivalence, inducing a better reduction. We show how to apply this approach using a symbolic representation of the transition relations of VHDL entities in order to check CTL properties.
We present in this work a concept of state equivalence that is defined with respect to a given CTL formula. This equivalence is used to reduce the size of each component FSM so that their product will be smaller. Contrary of strong bisimulation, it does not preserve all CTL formulae, so we can expect to compute coarser equivalence, inducing a better reduction. We show how to apply this approach using a symbolic representation of the transition relations of VHDL entities in order to check CTL properties.