Probabilistic Symbolic Simulation and Verification with ⊕-OBDDs
Identifieur interne : 001240 ( Istex/Corpus ); précédent : 001239; suivant : 001241Probabilistic Symbolic Simulation and Verification with ⊕-OBDDs
Auteurs : Christoph Meinel ; Harald SackSource :
- Electronic Notes in Theoretical Computer Science [ 1571-0661 ] ; 1999.
Abstract
Ordered Binary Decision Diagrams (OBDDs) have already proved useful in the verification of combinational and sequential circuits. Due to limitations of the descriptive power of OBDDs several more general models of Binary Decision Diagrams have been studied. In this paper, ⊕-OBDDs - also known as Mod2OBDDs - in respect to their ability to serve as a tool for combinational verification are considered. Besides the application of ⊕-OBDDs, the more general problem of how to exploit the inherent potential of ⊕-OBDDs more efficiently is addressed.
Url:
DOI: 10.1016/S1571-0661(05)80601-2
Links to Exploration step
ISTEX:F762C0EAE021FA53E125EB7E787DBCC707888893Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Probabilistic Symbolic Simulation and Verification with ⊕-OBDDs</title><author><name sortKey="Meinel, Christoph" sort="Meinel, Christoph" uniqKey="Meinel C" first="Christoph" last="Meinel">Christoph Meinel</name><affiliation><mods:affiliation>FB IV — Informatik, Universität Trier D-54286 Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: meinel@uni-trier.de</mods:affiliation></affiliation></author><author><name sortKey="Sack, Harald" sort="Sack, Harald" uniqKey="Sack H" first="Harald" last="Sack">Harald Sack</name><affiliation><mods:affiliation>FB IV — Informatik, Universität Trier D-54286 Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: meinel@uni-trier.de</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:F762C0EAE021FA53E125EB7E787DBCC707888893</idno><date when="1999" year="1999">1999</date><idno type="doi">10.1016/S1571-0661(05)80601-2</idno><idno type="url">https://api.istex.fr/document/F762C0EAE021FA53E125EB7E787DBCC707888893/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">001240</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001240</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a">Probabilistic Symbolic Simulation and Verification with ⊕-OBDDs</title><author><name sortKey="Meinel, Christoph" sort="Meinel, Christoph" uniqKey="Meinel C" first="Christoph" last="Meinel">Christoph Meinel</name><affiliation><mods:affiliation>FB IV — Informatik, Universität Trier D-54286 Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: meinel@uni-trier.de</mods:affiliation></affiliation></author><author><name sortKey="Sack, Harald" sort="Sack, Harald" uniqKey="Sack H" first="Harald" last="Sack">Harald Sack</name><affiliation><mods:affiliation>FB IV — Informatik, Universität Trier D-54286 Trier, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: meinel@uni-trier.de</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j">Electronic Notes in Theoretical Computer Science</title><title level="j" type="abbrev">ENTCS</title><idno type="ISSN">1571-0661</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="1999">1999</date><biblScope unit="volume">22</biblScope><biblScope unit="supplement">C</biblScope><biblScope unit="page" from="156">156</biblScope><biblScope unit="page" to="170">170</biblScope></imprint><idno type="ISSN">1571-0661</idno></series><idno type="istex">F762C0EAE021FA53E125EB7E787DBCC707888893</idno><idno type="DOI">10.1016/S1571-0661(05)80601-2</idno><idno type="PII">S1571-0661(05)80601-2</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">1571-0661</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Ordered Binary Decision Diagrams (OBDDs) have already proved useful in the verification of combinational and sequential circuits. Due to limitations of the descriptive power of OBDDs several more general models of Binary Decision Diagrams have been studied. In this paper, ⊕-OBDDs - also known as Mod2OBDDs - in respect to their ability to serve as a tool for combinational verification are considered. Besides the application of ⊕-OBDDs, the more general problem of how to exploit the inherent potential of ⊕-OBDDs more efficiently is addressed.</div></front></TEI><istex><corpusName>elsevier</corpusName><author><json:item><name>Christoph Meinel</name><affiliations><json:string>FB IV — Informatik, Universität Trier D-54286 Trier, Germany</json:string><json:string>E-mail: meinel@uni-trier.de</json:string></affiliations></json:item><json:item><name>Harald Sack</name><affiliations><json:string>FB IV — Informatik, Universität Trier D-54286 Trier, Germany</json:string><json:string>E-mail: meinel@uni-trier.de</json:string></affiliations></json:item></author><language><json:string>eng</json:string></language><originalGenre><json:string>Full-length article</json:string></originalGenre><abstract>Ordered Binary Decision Diagrams (OBDDs) have already proved useful in the verification of combinational and sequential circuits. Due to limitations of the descriptive power of OBDDs several more general models of Binary Decision Diagrams have been studied. In this paper, ⊕-OBDDs - also known as Mod2OBDDs - in respect to their ability to serve as a tool for combinational verification are considered. Besides the application of ⊕-OBDDs, the more general problem of how to exploit the inherent potential of ⊕-OBDDs more efficiently is addressed.</abstract><qualityIndicators><score>6.276</score><pdfVersion>1.4</pdfVersion><pdfPageSize>612 x 792 pts (letter)</pdfPageSize><refBibsNative>true</refBibsNative><keywordCount>0</keywordCount><abstractCharCount>546</abstractCharCount><pdfWordCount>4768</pdfWordCount><pdfCharCount>26204</pdfCharCount><pdfPageCount>15</pdfPageCount><abstractWordCount>84</abstractWordCount></qualityIndicators><title>Probabilistic Symbolic Simulation and Verification with ⊕-OBDDs</title><pii><json:string>S1571-0661(05)80601-2</json:string></pii><refBibs><json:item><author><json:item><name>M. Blum</name></json:item><json:item><name>A.K. Chandra</name></json:item><json:item><name>M.N. Wegman</name></json:item></author><host><volume>10</volume><pages><last>82</last><first>80</first></pages><issue>2</issue><author></author><title>Information Processing Letters</title></host><title>Equivalence of Free Boolean Graphs Can be Decided Probabilistically in Polynomial Time</title></json:item><json:item><host><author></author><title>Ordered Binary Decision Diagrams for Optimization in Symbolic Switch-Level Analysis of MOS Circuits</title></host></json:item><json:item><author><json:item><name>K.S. Brace</name></json:item><json:item><name>R.L. Rudell</name></json:item><json:item><name>R.E. Bryant</name></json:item></author><host><pages><last>45</last><first>40</first></pages><author></author><title>27th ACM/IEEE Design Automation Conference</title></host><title>Efficient Implementation of a BDD Package</title></json:item><json:item><author><json:item><name>R.E. Bryant</name></json:item></author><host><volume>40</volume><pages><last>213</last><first>205</first></pages><issue>2</issue><author></author><title>IEEE Transactions on Computers</title></host><title>On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication</title></json:item><json:item><author><json:item><name>J. Gergov</name></json:item><json:item><name>Ch Meinel</name></json:item></author><host><pages><last>585</last><first>576</first></pages><author></author><title>Proc. of the 10th annual Symposium on Theoretical Aspects of Computer Science, volume 665 of LNCS</title></host><title>Frontiers of Feasible and Probabilistic Feasible Boolean Manipulation with Branching Programs</title></json:item><json:item><author><json:item><name>J. Gergov</name></json:item><json:item><name>Ch Meinel</name></json:item></author><host><author></author><title>Formal Methods in System Design</title></host><serie><author></author><title>Formal Methods in System Design</title></serie><title>Mod2-OBDDs: A Data Structure that Generalizes EXOR-Sum-of-Products and Ordered Binary Decision Diagrams</title></json:item><json:item><author><json:item><name> The VIS Group</name></json:item></author><host><pages><last>432</last><first>428</first></pages><author></author><title>In Proc. of the 8th Int. Conference on Computer Aided Verification, number 1102 in Lecture Notes in Computer Science</title></host><title>VIS: A system for Verification and Synthesis</title></json:item><json:item><author><json:item><name>J. Jain</name></json:item><json:item><name>J. Bitner</name></json:item><json:item><name>D.S. Fussel</name></json:item><json:item><name>J. Abraham</name></json:item></author><host><volume>volume 1</volume><pages><last>117</last><first>63</first></pages><author></author><title>Formal Methods in System Design</title></host><title>Probabilistic Verification of Boolean Functions</title></json:item><json:item><author><json:item><name>J.-C. Madre</name></json:item><json:item><name>J.-P. Billon</name></json:item></author><host><pages><last>313</last><first>308</first></pages><author></author><title>Proc. of the 25th ACM/IEEE Design Automation Conference</title></host><title>Proving Circuit Correctness Using Formal Comparison Between Expected and Extracted Behaviour</title></json:item><json:item><host><author></author><title>Modified Branching Programs and Their Computational Power volume 370 of LNCS.</title></host></json:item><json:item><host><author></author><title>Algorithms and Data Structures in VLSI Design</title></host></json:item><json:item><author><json:item><name>S. Waack</name></json:item></author><host><author></author><title>In Proc. of the 14th Symposium on Theoretical Aspects of Computer Science, volume 1200 of LNCS.</title></host><title>On the Descriptive and Algorithmic Power of Parity Ordered Binary Decision Diagrams</title></json:item></refBibs><genre><json:string>research-article</json:string></genre><serie><volume>volume 8</volume><pages><last>282</last><first>273</first></pages><language><json:string>unknown</json:string></language><title>Formal Methods in System Design</title></serie><host><volume>22</volume><pii><json:string>S1571-0661(00)X0298-8</json:string></pii><editor><json:item><name>Christel Baier</name></json:item><json:item><name>Michael Huth</name></json:item><json:item><name>Marta Kwiatkowska</name></json:item><json:item><name>Mark Ryan</name></json:item></editor><pages><last>170</last><first>156</first></pages><conference><json:item><name>PROBMIV'98, First International Workshop on Probabilistic Methods in Verification, Indianapolis, Indiana, USA 19980619 19980620</name></json:item></conference><issn><json:string>1571-0661</json:string></issn><genre><json:string>journal</json:string></genre><language><json:string>unknown</json:string></language><title>Electronic Notes in Theoretical Computer Science</title><publicationDate>1999</publicationDate></host><categories><wos></wos><scienceMetrix><json:string>applied sciences</json:string><json:string>information & communication technologies</json:string><json:string>computation theory & mathematics</json:string></scienceMetrix></categories><publicationDate>1999</publicationDate><copyrightDate>1999</copyrightDate><doi><json:string>10.1016/S1571-0661(05)80601-2</json:string></doi><id>F762C0EAE021FA53E125EB7E787DBCC707888893</id><score>0.8163764</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/document/F762C0EAE021FA53E125EB7E787DBCC707888893/fulltext/pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/document/F762C0EAE021FA53E125EB7E787DBCC707888893/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/F762C0EAE021FA53E125EB7E787DBCC707888893/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a">Probabilistic Symbolic Simulation and Verification with ⊕-OBDDs</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher>ELSEVIER</publisher><availability><p>©1999 Elsevier B.V.</p></availability><date>1999</date></publicationStmt><notesStmt><note type="content">Section title: Articles</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a">Probabilistic Symbolic Simulation and Verification with ⊕-OBDDs</title><author xml:id="author-1"><persName><forename type="first">Christoph</forename><surname>Meinel</surname></persName><email>meinel@uni-trier.de</email><affiliation>FB IV — Informatik, Universität Trier D-54286 Trier, Germany</affiliation></author><author xml:id="author-2"><persName><forename type="first">Harald</forename><surname>Sack</surname></persName><email>meinel@uni-trier.de</email><affiliation>FB IV — Informatik, Universität Trier D-54286 Trier, Germany</affiliation></author></analytic><monogr><title level="j">Electronic Notes in Theoretical Computer Science</title><title level="j" type="abbrev">ENTCS</title><idno type="pISSN">1571-0661</idno><idno type="PII">S1571-0661(00)X0298-8</idno><meeting><addName>PROBMIV'98, First International Workshop on Probabilistic Methods in Verification, Indianapolis, Indiana, USA</addName><date>19980619</date><date>19980620</date></meeting><editor><persName>Christel Baier</persName></editor><editor><persName>Michael Huth</persName></editor><editor><persName>Marta Kwiatkowska</persName></editor><editor><persName>Mark Ryan</persName></editor><imprint><publisher>ELSEVIER</publisher><date type="published" when="1999"></date><biblScope unit="volume">22</biblScope><biblScope unit="supplement">C</biblScope><biblScope unit="page" from="156">156</biblScope><biblScope unit="page" to="170">170</biblScope></imprint></monogr><idno type="istex">F762C0EAE021FA53E125EB7E787DBCC707888893</idno><idno type="DOI">10.1016/S1571-0661(05)80601-2</idno><idno type="PII">S1571-0661(05)80601-2</idno></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>1999</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Ordered Binary Decision Diagrams (OBDDs) have already proved useful in the verification of combinational and sequential circuits. Due to limitations of the descriptive power of OBDDs several more general models of Binary Decision Diagrams have been studied. In this paper, ⊕-OBDDs - also known as Mod2OBDDs - in respect to their ability to serve as a tool for combinational verification are considered. Besides the application of ⊕-OBDDs, the more general problem of how to exploit the inherent potential of ⊕-OBDDs more efficiently is addressed.</p></abstract></profileDesc><revisionDesc><change when="1999">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/document/F762C0EAE021FA53E125EB7E787DBCC707888893/fulltext/txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Elsevier, elements deleted: tail" wicri:toSee="Element #text; element #text; element #text"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//ES//DTD journal article DTD version 4.5.2//EN//XML" URI="art452.dtd" name="istex:docType"></istex:docType><istex:document><converted-article version="4.5.2" docsubtype="fla"> <item-info> <jid>ENTCS</jid> <aid>601</aid> <ce:pii>S1571-0661(05)80601-2</ce:pii> <ce:doi>10.1016/S1571-0661(05)80601-2</ce:doi> <ce:copyright type="full-transfer" year="1999">Elsevier B.V.</ce:copyright> </item-info> <head> <ce:dochead> <ce:textfn>Articles</ce:textfn> </ce:dochead> <ce:title>Probabilistic Symbolic Simulation and Verification with ⊕-OBDDs</ce:title> <ce:author-group> <ce:author> <ce:given-name>Christoph</ce:given-name> <ce:surname>Meinel</ce:surname> <ce:e-address>meinel@uni-trier.de</ce:e-address> </ce:author> <ce:author> <ce:given-name>Harald</ce:given-name> <ce:surname>Sack</ce:surname> <ce:e-address>sack@uni-trier.de</ce:e-address> </ce:author> <ce:affiliation> <ce:textfn>FB IV — Informatik, Universität Trier D-54286 Trier, Germany</ce:textfn> </ce:affiliation> </ce:author-group> <ce:abstract> <ce:section-title>Abstract</ce:section-title> <ce:abstract-sec> <ce:simple-para>Ordered Binary Decision Diagrams (OBDDs) have already proved useful in the verification of combinational and sequential circuits. Due to limitations of the descriptive power of OBDDs several more general models of Binary Decision Diagrams have been studied. In this paper, ⊕-OBDDs - also known as Mod2OBDDs - in respect to their ability to serve as a tool for combinational verification are considered. Besides the application of ⊕-OBDDs, the more general problem of how to exploit the inherent potential of ⊕-OBDDs more efficiently is addressed.</ce:simple-para> </ce:abstract-sec> </ce:abstract> </head> </converted-article></istex:document></istex:metadataXml><mods version="3.6"><titleInfo><title>Probabilistic Symbolic Simulation and Verification with ⊕-OBDDs</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Probabilistic Symbolic Simulation and Verification with ⊕-OBDDs</title></titleInfo><name type="personal"><namePart type="given">Christoph</namePart><namePart type="family">Meinel</namePart><affiliation>FB IV — Informatik, Universität Trier D-54286 Trier, Germany</affiliation><affiliation>E-mail: meinel@uni-trier.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Harald</namePart><namePart type="family">Sack</namePart><affiliation>FB IV — Informatik, Universität Trier D-54286 Trier, Germany</affiliation><affiliation>E-mail: meinel@uni-trier.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="Full-length article"></genre><originInfo><publisher>ELSEVIER</publisher><dateIssued encoding="w3cdtf">1999</dateIssued><copyrightDate encoding="w3cdtf">1999</copyrightDate></originInfo><language><languageTerm type="code" authority="iso639-2b">eng</languageTerm><languageTerm type="code" authority="rfc3066">en</languageTerm></language><physicalDescription><internetMediaType>text/html</internetMediaType></physicalDescription><abstract lang="en">Ordered Binary Decision Diagrams (OBDDs) have already proved useful in the verification of combinational and sequential circuits. Due to limitations of the descriptive power of OBDDs several more general models of Binary Decision Diagrams have been studied. In this paper, ⊕-OBDDs - also known as Mod2OBDDs - in respect to their ability to serve as a tool for combinational verification are considered. Besides the application of ⊕-OBDDs, the more general problem of how to exploit the inherent potential of ⊕-OBDDs more efficiently is addressed.</abstract><note type="content">Section title: Articles</note><relatedItem type="host"><titleInfo><title>Electronic Notes in Theoretical Computer Science</title></titleInfo><titleInfo type="abbreviated"><title>ENTCS</title></titleInfo><name type="conference"><namePart>PROBMIV'98, First International Workshop on Probabilistic Methods in Verification, Indianapolis, Indiana, USA</namePart><namePart type="date">19980619</namePart><namePart type="date">19980620</namePart></name><name type="personal"><namePart>Christel Baier</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart>Michael Huth</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart>Marta Kwiatkowska</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart>Mark Ryan</namePart><role><roleTerm type="text">editor</roleTerm></role></name><genre type="journal">journal</genre><originInfo><dateIssued encoding="w3cdtf">1999</dateIssued></originInfo><identifier type="ISSN">1571-0661</identifier><identifier type="PII">S1571-0661(00)X0298-8</identifier><part><date>1999</date><detail type="issue"><title>PROBMIV'98, First International Workshop on Probabilistic Methods in Verification, Indianapolis, Indiana, USA</title></detail><detail type="volume"><number>22</number><caption>vol.</caption></detail><detail type="supplement"><number>C</number><caption>Suppl.</caption></detail><extent unit="issue pages"><start>1</start><end>207</end></extent><extent unit="pages"><start>156</start><end>170</end></extent></part></relatedItem><identifier type="istex">F762C0EAE021FA53E125EB7E787DBCC707888893</identifier><identifier type="DOI">10.1016/S1571-0661(05)80601-2</identifier><identifier type="PII">S1571-0661(05)80601-2</identifier><accessCondition type="use and reproduction" contentType="copyright">©1999 Elsevier B.V.</accessCondition><recordInfo><recordContentSource>ELSEVIER</recordContentSource><recordOrigin>Elsevier B.V., ©1999</recordOrigin></recordInfo></mods></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Rhénanie/explor/UnivTrevesV1/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001240 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001240 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Rhénanie
|area= UnivTrevesV1
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:F762C0EAE021FA53E125EB7E787DBCC707888893
|texte= Probabilistic Symbolic Simulation and Verification with ⊕-OBDDs
}}
| This area was generated with Dilib version V0.6.31. |  |