Difference between revisions of "Publications:Model checking Verilog descriptions of cell libraries"
From CERES
(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...") |
(No difference)
|
Latest revision as of 04:43, 26 June 2014
| Title | Model checking Verilog descriptions of cell libraries |
|---|---|
| Author | Matthias Raffelsieper and Jan-Willem Roorda and Mohammad Reza Mousavi |
| Year | 2009 |
| PublicationType | Conference Paper |
| Journal | |
| HostPublication | 2009 Ninth International Conference on Application of Concurrency to System Design : Proceedings |
| DOI | http://dx.doi.org/10.1109/ACSD.2009.18 |
| Conference | 9th International Conference on Application of Concurrency to System Design, Augsburg, GERMANY, JUL 01-03, 2009 |
| Diva url | http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:584680 |
| Abstract | 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. |
