Publications:Model checking Verilog descriptions of cell libraries
From CERES
| 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. |
