Loading…
Equivalence checking of partial designs using dependency quantified Boolean formulae
We consider the partial equivalence checking problem (PEC), i. e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the q...
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Conference Proceeding |
| Language: | English |
| Subjects: | |
| Online Access: | Request full text |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| cited_by | |
|---|---|
| cites | |
| container_end_page | 403 |
| container_issue | |
| container_start_page | 396 |
| container_title | |
| container_volume | |
| creator | Gitina, Karina Reimer, Sven Sauer, Matthias Wimmer, Ralf Scholl, Christoph Becker, Bernd |
| description | We consider the partial equivalence checking problem (PEC), i. e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied. Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC.We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far. |
| doi_str_mv | 10.1109/ICCD.2013.6657071 |
| format | conference_proceeding |
| fullrecord | <record><control><sourceid>ieee_CHZPO</sourceid><recordid>TN_cdi_ieee_primary_6657071</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><ieee_id>6657071</ieee_id><sourcerecordid>6657071</sourcerecordid><originalsourceid>FETCH-LOGICAL-i175t-41b7746586c25977f2d085a56e63c075b06d94643354d2fb56e56d6e0badadbb3</originalsourceid><addsrcrecordid>eNotkMFOwkAURUejiYh8gHEzP1B805l5r7PUikpC4gbXZNp5xdHSQktN-HswsjqLc3IXV4h7BVOlwD3O8_xlmoLSU0RLQOpCTBxlypBzqcsILsUotYQJOodXYqQAdYIGzI247ftvAMi0opFYznZD_PU1NyXL8ovLn9isZVvJre_20dcycB_XTS-H_k8E3nITTvFB7gbf7GMVOcjntq3ZN7Jqu81Qe74T15Wve56cORafr7Nl_p4sPt7m-dMiiYrsPjGqIDJoMyxT64iqNEBmvUVGXQLZAjA4g0Zra0JaFSdhMSBD4YMPRaHH4uF_NzLzatvFje8Oq_Mh-ghd2lMW</addsrcrecordid><sourcetype>Publisher</sourcetype><iscdi>true</iscdi><recordtype>conference_proceeding</recordtype></control><display><type>conference_proceeding</type><title>Equivalence checking of partial designs using dependency quantified Boolean formulae</title><source>IEEE Xplore All Conference Series</source><creator>Gitina, Karina ; Reimer, Sven ; Sauer, Matthias ; Wimmer, Ralf ; Scholl, Christoph ; Becker, Bernd</creator><creatorcontrib>Gitina, Karina ; Reimer, Sven ; Sauer, Matthias ; Wimmer, Ralf ; Scholl, Christoph ; Becker, Bernd</creatorcontrib><description>We consider the partial equivalence checking problem (PEC), i. e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied. Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC.We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far.</description><identifier>ISSN: 1063-6404</identifier><identifier>EISSN: 2576-6996</identifier><identifier>EISBN: 9781479929870</identifier><identifier>EISBN: 1479929875</identifier><identifier>DOI: 10.1109/ICCD.2013.6657071</identifier><language>eng</language><publisher>IEEE</publisher><subject>Algorithm design and analysis ; Approximation algorithms ; Approximation methods ; Combinational circuits ; Complexity theory ; Logic gates ; System analysis and design</subject><ispartof>2013 IEEE 31st International Conference on Computer Design (ICCD), 2013, p.396-403</ispartof><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktohtml>$$Uhttps://ieeexplore.ieee.org/document/6657071$$EHTML$$P50$$Gieee$$H</linktohtml><link.rule.ids>309,310,780,784,789,790,27925,54555,54932</link.rule.ids><linktorsrc>$$Uhttps://ieeexplore.ieee.org/document/6657071$$EView_record_in_IEEE$$FView_record_in_$$GIEEE</linktorsrc></links><search><creatorcontrib>Gitina, Karina</creatorcontrib><creatorcontrib>Reimer, Sven</creatorcontrib><creatorcontrib>Sauer, Matthias</creatorcontrib><creatorcontrib>Wimmer, Ralf</creatorcontrib><creatorcontrib>Scholl, Christoph</creatorcontrib><creatorcontrib>Becker, Bernd</creatorcontrib><title>Equivalence checking of partial designs using dependency quantified Boolean formulae</title><title>2013 IEEE 31st International Conference on Computer Design (ICCD)</title><addtitle>ICCD</addtitle><description>We consider the partial equivalence checking problem (PEC), i. e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied. Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC.We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far.</description><subject>Algorithm design and analysis</subject><subject>Approximation algorithms</subject><subject>Approximation methods</subject><subject>Combinational circuits</subject><subject>Complexity theory</subject><subject>Logic gates</subject><subject>System analysis and design</subject><issn>1063-6404</issn><issn>2576-6996</issn><isbn>9781479929870</isbn><isbn>1479929875</isbn><fulltext>true</fulltext><rsrctype>conference_proceeding</rsrctype><creationdate>2013</creationdate><recordtype>conference_proceeding</recordtype><sourceid>6IE</sourceid><recordid>eNotkMFOwkAURUejiYh8gHEzP1B805l5r7PUikpC4gbXZNp5xdHSQktN-HswsjqLc3IXV4h7BVOlwD3O8_xlmoLSU0RLQOpCTBxlypBzqcsILsUotYQJOodXYqQAdYIGzI247ftvAMi0opFYznZD_PU1NyXL8ovLn9isZVvJre_20dcycB_XTS-H_k8E3nITTvFB7gbf7GMVOcjntq3ZN7Jqu81Qe74T15Wve56cORafr7Nl_p4sPt7m-dMiiYrsPjGqIDJoMyxT64iqNEBmvUVGXQLZAjA4g0Zra0JaFSdhMSBD4YMPRaHH4uF_NzLzatvFje8Oq_Mh-ghd2lMW</recordid><startdate>201310</startdate><enddate>201310</enddate><creator>Gitina, Karina</creator><creator>Reimer, Sven</creator><creator>Sauer, Matthias</creator><creator>Wimmer, Ralf</creator><creator>Scholl, Christoph</creator><creator>Becker, Bernd</creator><general>IEEE</general><scope>6IE</scope><scope>6IH</scope><scope>CBEJK</scope><scope>RIE</scope><scope>RIO</scope></search><sort><creationdate>201310</creationdate><title>Equivalence checking of partial designs using dependency quantified Boolean formulae</title><author>Gitina, Karina ; Reimer, Sven ; Sauer, Matthias ; Wimmer, Ralf ; Scholl, Christoph ; Becker, Bernd</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-i175t-41b7746586c25977f2d085a56e63c075b06d94643354d2fb56e56d6e0badadbb3</frbrgroupid><rsrctype>conference_proceedings</rsrctype><prefilter>conference_proceedings</prefilter><language>eng</language><creationdate>2013</creationdate><topic>Algorithm design and analysis</topic><topic>Approximation algorithms</topic><topic>Approximation methods</topic><topic>Combinational circuits</topic><topic>Complexity theory</topic><topic>Logic gates</topic><topic>System analysis and design</topic><toplevel>online_resources</toplevel><creatorcontrib>Gitina, Karina</creatorcontrib><creatorcontrib>Reimer, Sven</creatorcontrib><creatorcontrib>Sauer, Matthias</creatorcontrib><creatorcontrib>Wimmer, Ralf</creatorcontrib><creatorcontrib>Scholl, Christoph</creatorcontrib><creatorcontrib>Becker, Bernd</creatorcontrib><collection>IEEE Electronic Library (IEL) Conference Proceedings</collection><collection>IEEE Proceedings Order Plan (POP) 1998-present by volume</collection><collection>IEEE Xplore All Conference Proceedings</collection><collection>IEEE/IET Electronic Library (IEL)</collection><collection>IEEE Proceedings Order Plans (POP) 1998-present</collection></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext_linktorsrc</fulltext></delivery><addata><au>Gitina, Karina</au><au>Reimer, Sven</au><au>Sauer, Matthias</au><au>Wimmer, Ralf</au><au>Scholl, Christoph</au><au>Becker, Bernd</au><format>book</format><genre>proceeding</genre><ristype>CONF</ristype><atitle>Equivalence checking of partial designs using dependency quantified Boolean formulae</atitle><btitle>2013 IEEE 31st International Conference on Computer Design (ICCD)</btitle><stitle>ICCD</stitle><date>2013-10</date><risdate>2013</risdate><spage>396</spage><epage>403</epage><pages>396-403</pages><issn>1063-6404</issn><eissn>2576-6996</eissn><eisbn>9781479929870</eisbn><eisbn>1479929875</eisbn><abstract>We consider the partial equivalence checking problem (PEC), i. e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied. Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC.We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far.</abstract><pub>IEEE</pub><doi>10.1109/ICCD.2013.6657071</doi><tpages>8</tpages></addata></record> |
| fulltext | fulltext_linktorsrc |
| identifier | ISSN: 1063-6404 |
| ispartof | 2013 IEEE 31st International Conference on Computer Design (ICCD), 2013, p.396-403 |
| issn | 1063-6404 2576-6996 |
| language | eng |
| recordid | cdi_ieee_primary_6657071 |
| source | IEEE Xplore All Conference Series |
| subjects | Algorithm design and analysis Approximation algorithms Approximation methods Combinational circuits Complexity theory Logic gates System analysis and design |
| title | Equivalence checking of partial designs using dependency quantified Boolean formulae |
| url | http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-29T00%3A15%3A53IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-ieee_CHZPO&rft_val_fmt=info:ofi/fmt:kev:mtx:book&rft.genre=proceeding&rft.atitle=Equivalence%20checking%20of%20partial%20designs%20using%20dependency%20quantified%20Boolean%20formulae&rft.btitle=2013%20IEEE%2031st%20International%20Conference%20on%20Computer%20Design%20(ICCD)&rft.au=Gitina,%20Karina&rft.date=2013-10&rft.spage=396&rft.epage=403&rft.pages=396-403&rft.issn=1063-6404&rft.eissn=2576-6996&rft_id=info:doi/10.1109/ICCD.2013.6657071&rft.eisbn=9781479929870&rft.eisbn_list=1479929875&rft_dat=%3Cieee_CHZPO%3E6657071%3C/ieee_CHZPO%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-i175t-41b7746586c25977f2d085a56e63c075b06d94643354d2fb56e56d6e0badadbb3%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rft_ieee_id=6657071&rfr_iscdi=true |