Verilog2SMV: A Tool for Word-level Verification
The work
| Authors | Ahmed Irfan; Alessandro Cimatti; Alberto Griggio; Marco Roveri; Roberto Sebastiani |
|---|---|
| Editors | |
| Type | misc |
| Year | 2016 |
| Citekey | irfan2016verilog2smv |
Where it appeared
| Published in | Design, Automation, and Test in Europe |
|---|---|
| Pages | 1156--1159 |
Identifiers
| DOI | 10.3850/9783981537079_0765 |
|---|---|
| OpenAlex | W2345650502 |
Access
| Landing page | https://doi.org/10.3850/9783981537079_0765 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
Verification is an essential step of the hardware design lifecycle. Usually verification is done at the gate level (Boolean level). We present verilog2smv, a tool that generates word-level model checking problems from Verilog designs augmented with assertions. A key aspect of our tool is that memories in the designs are treated without any form of abstraction. verilog2smv can be used for RTL verification by chaining with a word-level model checker like NUXMV. To this extent, we present also some experimental results over Verilog verification benchmarks, using verilog2smv+NUXMV as a tool-chain.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-24 22:13 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{irfan2016verilog2smv,
title = {Verilog2SMV: A Tool for Word-level Verification},
author = {Ahmed Irfan and Alessandro Cimatti and Alberto Griggio and Marco Roveri and Roberto Sebastiani},
year = {2016},
journal = {Design, Automation, and Test in Europe},
pages = {1156--1159},
doi = {10.3850/9783981537079_0765},
}
This record lives at https://refs.drheap.org/irfan2016verilog2smv/ and will keep doing so.