https://wiki.hh.se/ceres/index.php?action=history&feed=atom&title=Publications%3AModel_checking_Verilog_descriptions_of_cell_librariesPublications:Model checking Verilog descriptions of cell libraries - Revision history2026-05-23T05:48:47ZRevision history for this page on the wikiMediaWiki 1.22.6https://wiki.hh.se/ceres/index.php?title=Publications:Model_checking_Verilog_descriptions_of_cell_libraries&diff=4158&oldid=prevSlawek: Created page with "<div style='display: none'> == Do not edit this section == </div> {{PublicationSetupTemplate|Author=Matthias Raffelsieper, Jan-Willem Roorda, Mohammad Reza Mousavi |PID=584680..."2014-06-26T03:43:50Z<p>Created page with "<div style='display: none'> == Do not edit this section == </div> {{PublicationSetupTemplate|Author=Matthias Raffelsieper, Jan-Willem Roorda, Mohammad Reza Mousavi |PID=584680..."</p>
<p><b>New page</b></p><div><div style='display: none'><br />
== Do not edit this section ==<br />
</div><br />
{{PublicationSetupTemplate|Author=Matthias Raffelsieper, Jan-Willem Roorda, Mohammad Reza Mousavi<br />
|PID=584680<br />
|Name=Raffelsieper, Matthias (Department of Computer Science TU Eindhoven, P.O. Box 513 Eindhoven, The Netherlands);Roorda, Jan-Willem (Fenix Design Automation P.O. Box 920 Eindhoven, The Netherlands);Mousavi, Mohammad Reza [mohmou] (Department of Computer Science TU Eindhoven, P.O. Box 513 Eindhoven, The Netherlands)<br />
|Title=Model checking Verilog descriptions of cell libraries<br />
|PublicationType=Conference Paper<br />
|ContentType=Refereegranskat<br />
|Language=eng<br />
|Journal=<br />
|JournalISSN=<br />
|Status=<br />
|Volume=<br />
|Issue=<br />
|HostPublication=2009 Ninth International Conference on Application of Concurrency to System Design : Proceedings<br />
|Conference=9th International Conference on Application of Concurrency to System Design, Augsburg, GERMANY, JUL 01-03, 2009<br />
|StartPage=128<br />
|EndPage=137<br />
|Year=2009<br />
|Edition=<br />
|Pages=<br />
|City=Los Alamitos, Calif.<br />
|Publisher=IEEE Computer Society<br />
|Series=<br />
|SeriesISSN=<br />
|ISBN=978-0-7695-3697-2<br />
|Urls=<br />
|ISRN=<br />
|DOI=http://dx.doi.org/10.1109/ACSD.2009.18<br />
|ISI=000275024600015<br />
|PMID=<br />
|ScopusId=2-s2.0-70549112299<br />
|NBN=urn:nbn:se:hh:diva-20509<br />
|LocalId=<br />
|ArchiveNumber=<br />
|Keywords=Cell library;Equivalence checking;Formal semantics;Netlist;SMV model;Symbolic model checking;Transition system;Verilog<br />
|Categories=Data- och informationsvetenskap (102)<br />
|ResearchSubjects=<br />
|Projects=<br />
|Notes=<br />
|Abstract=<p>We present a formal semantics for a subset of Verilog, commonly used to describe cell libraries, in terms of transition systems. Such transition systems can serve as input to symbolic model checking, for example equivalence checking with a transistor netlist description. We implement our formal semantics as an encoding from the subset of Verilog to the input language of the SMV model-checker. Experiments show that this approach is able to verify complete cell libraries.</p><br />
|Opponents=<br />
|Supervisors=<br />
|Examiners=<br />
|Patent=<br />
|ThesisLevel=<br />
|Credits=<br />
|Programme=<br />
|Subject=<br />
|Uppsok=<br />
|DefencePlace=<br />
|DefenceLanguage=<br />
|DefenceDate=<br />
|CreatedDate=2013-01-08<br />
|PublicationDate=2013-01-09<br />
|LastUpdated=2013-02-21<br />
|diva=http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:584680}}<br />
<div style='display: none'><br />
<br />
== Keep all hand-made modifications below ==<br />
</div>{{PublicationDisplayTemplate}}</div>Slawek