Speeding up image computation by using RTL information
Identifieur interne : 000C57 ( PascalFrancis/Checkpoint ); précédent : 000C56; suivant : 000C58Speeding up image computation by using RTL information
Auteurs : Christoph Meinel [Allemagne] ; Christian Stangier [Allemagne]Source :
- Lecture notes in computer science [ 0302-9743 ] ; 2000.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
Image computation is the core operation for optimization and formal verification of sequential systems like controllers or protocols. State exploration techniques based on OBDDs use a partitioned representation of the transition relation to keep the OBDD-sizes manageable. This paper presents a new approach that significantly increases the quality of the partitioning of the transition relation of controllers given in the hardware description language Verilog. The heuristic has been successfully applied to reachability analysis and symbolic model checking of real life designs, resulting in a significant reduction both in CPU time and memory consumption.
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
Pascal:01-0051918Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Speeding up image computation by using RTL information</title><author><name sortKey="Meinel, Christoph" sort="Meinel, Christoph" uniqKey="Meinel C" first="Christoph" last="Meinel">Christoph Meinel</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>FB Informatik, University of Trier</s1><s3>DEU</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Allemagne</country><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><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, Christian" sort="Stangier, Christian" uniqKey="Stangier C" first="Christian" last="Stangier">Christian Stangier</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>FB Informatik, University of Trier</s1><s3>DEU</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Allemagne</country><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></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">01-0051918</idno><date when="2000">2000</date><idno type="stanalyst">PASCAL 01-0051918 INIST</idno><idno type="RBID">Pascal:01-0051918</idno><idno type="wicri:Area/PascalFrancis/Corpus">000E73</idno><idno type="wicri:Area/PascalFrancis/Curation">000084</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000C57</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000C57</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Speeding up image computation by using RTL information</title><author><name sortKey="Meinel, Christoph" sort="Meinel, Christoph" uniqKey="Meinel C" first="Christoph" last="Meinel">Christoph Meinel</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>FB Informatik, University of Trier</s1><s3>DEU</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Allemagne</country><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><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, Christian" sort="Stangier, Christian" uniqKey="Stangier C" first="Christian" last="Stangier">Christian Stangier</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>FB Informatik, University of Trier</s1><s3>DEU</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></inist:fA14><country>Allemagne</country><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></analytic><series><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno><imprint><date when="2000">2000</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Binary decision diagram</term><term>Calculation</term><term>Controller</term><term>Description language</term><term>Formal verification</term><term>Image</term><term>Reachability</term><term>Sequential method</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Image</term><term>Calcul</term><term>Vérification formelle</term><term>Méthode séquentielle</term><term>Atteignabilité</term><term>Contrôleur</term><term>Langage description</term><term>Diagramme binaire décision</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Image computation is the core operation for optimization and formal verification of sequential systems like controllers or protocols. State exploration techniques based on OBDDs use a partitioned representation of the transition relation to keep the OBDD-sizes manageable. This paper presents a new approach that significantly increases the quality of the partitioning of the transition relation of controllers given in the hardware description language Verilog. The heuristic has been successfully applied to reachability analysis and symbolic model checking of real life designs, resulting in a significant reduction both in CPU time and memory consumption.</div></front></TEI><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0></fA01><fA05><s2>1954</s2></fA05><fA08 i1="01" i2="1" l="ENG"><s1>Speeding up image computation by using RTL information</s1></fA08><fA09 i1="01" i2="1" l="ENG"><s1>FMCAD 2000 : formal methods in computer-aided design : Austin TX, 1-3 November 2000</s1></fA09><fA11 i1="01" i2="1"><s1>MEINEL (Christoph)</s1></fA11><fA11 i1="02" i2="1"><s1>STANGIER (Christian)</s1></fA11><fA12 i1="01" i2="1"><s1>HUNT (Warren A.)</s1><s9>ed.</s9></fA12><fA12 i1="02" i2="1"><s1>JOHNSON (Steven D.)</s1><s9>ed.</s9></fA12><fA14 i1="01"><s1>FB Informatik, University of Trier</s1><s3>DEU</s3><sZ>1 aut.</sZ><sZ>2 aut.</sZ></fA14><fA20><s1>443-454</s1></fA20><fA21><s1>2000</s1></fA21><fA23 i1="01"><s0>ENG</s0></fA23><fA26 i1="01"><s0>3-540-41219-0</s0></fA26><fA43 i1="01"><s1>INIST</s1><s2>16343</s2><s5>354000090102820250</s5></fA43><fA44><s0>0000</s0><s1>© 2001 INIST-CNRS. All rights reserved.</s1></fA44><fA45><s0>11 ref.</s0></fA45><fA47 i1="01" i2="1"><s0>01-0051918</s0></fA47><fA60><s1>P</s1><s2>C</s2></fA60><fA61><s0>A</s0></fA61><fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0></fA64><fA66 i1="01"><s0>DEU</s0></fA66><fC01 i1="01" l="ENG"><s0>Image computation is the core operation for optimization and formal verification of sequential systems like controllers or protocols. State exploration techniques based on OBDDs use a partitioned representation of the transition relation to keep the OBDD-sizes manageable. This paper presents a new approach that significantly increases the quality of the partitioning of the transition relation of controllers given in the hardware description language Verilog. The heuristic has been successfully applied to reachability analysis and symbolic model checking of real life designs, resulting in a significant reduction both in CPU time and memory consumption.</s0></fC01><fC02 i1="01" i2="X"><s0>001D02A07</s0></fC02><fC02 i1="02" i2="X"><s0>001D02B04</s0></fC02><fC03 i1="01" i2="X" l="FRE"><s0>Image</s0><s5>01</s5></fC03><fC03 i1="01" i2="X" l="ENG"><s0>Image</s0><s5>01</s5></fC03><fC03 i1="01" i2="X" l="SPA"><s0>Imagen</s0><s5>01</s5></fC03><fC03 i1="02" i2="X" l="FRE"><s0>Calcul</s0><s5>02</s5></fC03><fC03 i1="02" i2="X" l="ENG"><s0>Calculation</s0><s5>02</s5></fC03><fC03 i1="02" i2="X" l="SPA"><s0>Cálculo</s0><s5>02</s5></fC03><fC03 i1="03" i2="3" l="FRE"><s0>Vérification formelle</s0><s5>03</s5></fC03><fC03 i1="03" i2="3" l="ENG"><s0>Formal verification</s0><s5>03</s5></fC03><fC03 i1="04" i2="X" l="FRE"><s0>Méthode séquentielle</s0><s5>04</s5></fC03><fC03 i1="04" i2="X" l="ENG"><s0>Sequential method</s0><s5>04</s5></fC03><fC03 i1="04" i2="X" l="SPA"><s0>Método secuencial</s0><s5>04</s5></fC03><fC03 i1="05" i2="X" l="FRE"><s0>Atteignabilité</s0><s5>05</s5></fC03><fC03 i1="05" i2="X" l="ENG"><s0>Reachability</s0><s5>05</s5></fC03><fC03 i1="05" i2="X" l="SPA"><s0>Asequibilidad</s0><s5>05</s5></fC03><fC03 i1="06" i2="X" l="FRE"><s0>Contrôleur</s0><s5>06</s5></fC03><fC03 i1="06" i2="X" l="ENG"><s0>Controller</s0><s5>06</s5></fC03><fC03 i1="06" i2="X" l="SPA"><s0>Supervisor</s0><s5>06</s5></fC03><fC03 i1="07" i2="X" l="FRE"><s0>Langage description</s0><s5>07</s5></fC03><fC03 i1="07" i2="X" l="ENG"><s0>Description language</s0><s5>07</s5></fC03><fC03 i1="07" i2="X" l="SPA"><s0>Lenguaje descripción</s0><s5>07</s5></fC03><fC03 i1="08" i2="X" l="FRE"><s0>Diagramme binaire décision</s0><s5>08</s5></fC03><fC03 i1="08" i2="X" l="ENG"><s0>Binary decision diagram</s0><s5>08</s5></fC03><fC03 i1="08" i2="X" l="SPA"><s0>Diagrama binaria decisión</s0><s5>08</s5></fC03><fN21><s1>029</s1></fN21></pA><pR><fA30 i1="01" i2="1" l="ENG"><s1>Formal methods in computer-aided design. International conference</s1><s2>3</s2><s3>Austin TX USA</s3><s4>2000-11-01</s4></fA30></pR></standard></inist><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, Christoph" sort="Meinel, Christoph" uniqKey="Meinel C" first="Christoph" last="Meinel">Christoph Meinel</name></region><name sortKey="Stangier, Christian" sort="Stangier, Christian" uniqKey="Stangier C" first="Christian" last="Stangier">Christian Stangier</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Rhénanie/explor/UnivTrevesV1/Data/PascalFrancis/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000C57 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Checkpoint/biblio.hfd -nk 000C57 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Rhénanie
|area= UnivTrevesV1
|flux= PascalFrancis
|étape= Checkpoint
|type= RBID
|clé= Pascal:01-0051918
|texte= Speeding up image computation by using RTL information
}}
| This area was generated with Dilib version V0.6.31. |  |