Speeding up symbolic model checking
Identifieur interne : 002333 ( Main/Exploration ); précédent : 002332; suivant : 002334Speeding up symbolic model checking
Auteurs : Christoph Meinel [Allemagne] ; C. Stangier [Allemagne]Source :
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
Model checking is a widely used technique in verification of sequential circuits, reactive systems, protocols, etc. Ordered Binary Decision Diagrams (OBDDs) allow a symbolic representation of the model, that may avoid the state space explosion problem of larger systems. Since the size of OBDDs and thus the computation time depends on the order of input variables, the verification may only succeed, if a ell suited variable order, is chosen. Since the requirements for the functions are changing, the variable order has to be adapted dynamically. Unfortunately. this reordering is often very time consuming, even without improving the OBDD representation. We present, a technique that substantially accelerates the reordering process hy using easily computable structural information about the represeated function. This technique does not increase OBDD size significantly.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 001030
- to stream PascalFrancis, to step Curation: 001764
- to stream PascalFrancis, to step Checkpoint: 000E56
- to stream Main, to step Merge: 002727
- to stream Main, to step Curation: 002333
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Speeding up symbolic model checking</title><author><name sortKey="Meinel, C" sort="Meinel, C" uniqKey="Meinel C" first="C." last="Meinel">Christoph Meinel</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>FB IV - Informatik, Universität Trier</s1><s2>54286 Trier</s2><s3>DEU</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Allemagne</country><wicri:noRegion>54286 Trier</wicri:noRegion><wicri:noRegion>Universität Trier</wicri:noRegion><wicri:noRegion>54286 Trier</wicri:noRegion><placeName><settlement type="city">Trèves (Allemagne)</settlement><region type="land" nuts="1">Rhénanie-Palatinat</region></placeName><orgName type="university">Université de Trèves</orgName></affiliation></author><author><name sortKey="Stangier, C" sort="Stangier, C" uniqKey="Stangier C" first="C." last="Stangier">C. Stangier</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>FB IV - Informatik, Universität Trier</s1><s2>54286 Trier</s2><s3>DEU</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Allemagne</country><wicri:noRegion>54286 Trier</wicri:noRegion><wicri:noRegion>Universität Trier</wicri:noRegion><wicri:noRegion>54286 Trier</wicri:noRegion></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">99-0245697</idno><date when="1998">1998</date><idno type="stanalyst">PASCAL 99-0245697 INIST</idno><idno type="RBID">Pascal:99-0245697</idno><idno type="wicri:Area/PascalFrancis/Corpus">001030</idno><idno type="wicri:Area/PascalFrancis/Curation">001764</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000E56</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000E56</idno><idno type="wicri:Area/Main/Merge">002727</idno><idno type="wicri:Area/Main/Curation">002333</idno><idno type="wicri:Area/Main/Exploration">002333</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Speeding up symbolic model checking</title><author><name sortKey="Meinel, C" sort="Meinel, C" uniqKey="Meinel C" first="C." last="Meinel">Christoph Meinel</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>FB IV - Informatik, Universität Trier</s1><s2>54286 Trier</s2><s3>DEU</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Allemagne</country><wicri:noRegion>54286 Trier</wicri:noRegion><wicri:noRegion>Universität Trier</wicri:noRegion><wicri:noRegion>54286 Trier</wicri:noRegion><placeName><settlement type="city">Trèves (Allemagne)</settlement><region type="land" nuts="1">Rhénanie-Palatinat</region></placeName><orgName type="university">Université de Trèves</orgName></affiliation></author><author><name sortKey="Stangier, C" sort="Stangier, C" uniqKey="Stangier C" first="C." last="Stangier">C. Stangier</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>FB IV - Informatik, Universität Trier</s1><s2>54286 Trier</s2><s3>DEU</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Allemagne</country><wicri:noRegion>54286 Trier</wicri:noRegion><wicri:noRegion>Universität Trier</wicri:noRegion><wicri:noRegion>54286 Trier</wicri:noRegion></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Binary decision diagram</term><term>Boolean operator</term><term>Computation time</term><term>Experimental result</term><term>Implementation</term><term>Integrated circuit</term><term>Modeling</term><term>Sequential circuit</term><term>State space</term><term>Symbolic representation</term><term>Verification</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Vérification</term><term>Circuit séquentiel</term><term>Diagramme binaire décision</term><term>Implémentation</term><term>Espace état</term><term>Modélisation</term><term>Temps calcul</term><term>Opérateur booléen</term><term>Résultat expérimental</term><term>Circuit intégré</term><term>Représentation symbolique</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Model checking is a widely used technique in verification of sequential circuits, reactive systems, protocols, etc. Ordered Binary Decision Diagrams (OBDDs) allow a symbolic representation of the model, that may avoid the state space explosion problem of larger systems. Since the size of OBDDs and thus the computation time depends on the order of input variables, the verification may only succeed, if a ell suited variable order, is chosen. Since the requirements for the functions are changing, the variable order has to be adapted dynamically. Unfortunately. this reordering is often very time consuming, even without improving the OBDD representation. We present, a technique that substantially accelerates the reordering process hy using easily computable structural information about the represeated function. This technique does not increase OBDD size significantly.</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>Rhénanie-Palatinat</li></region><settlement><li>Trèves (Allemagne)</li></settlement><orgName><li>Université de Trèves</li></orgName></list><tree><country name="Allemagne"><region name="Rhénanie-Palatinat"><name sortKey="Meinel, C" sort="Meinel, C" uniqKey="Meinel C" first="C." last="Meinel">Christoph Meinel</name></region><name sortKey="Stangier, C" sort="Stangier, C" uniqKey="Stangier C" first="C." last="Stangier">C. Stangier</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Rhénanie/explor/UnivTrevesV1/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002333 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 002333 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Rhénanie
|area= UnivTrevesV1
|flux= Main
|étape= Exploration
|type= RBID
|clé= Pascal:99-0245697
|texte= Speeding up symbolic model checking
}}
| This area was generated with Dilib version V0.6.31. |  |