A scalable symbolic simulator for Verilog RTL
DSpace at IIT Bombay
View Archive InfoField | Value | |
Title |
A scalable symbolic simulator for Verilog RTL
|
|
Creator |
SUNKARI, SASIDHAR
CHAKRABORTY, SUPRATIK VEDULA, VIVEKANANDA MANEPARAMBIL, KAILASNATH |
|
Subject |
circuit simulation
formal verification hardware description languages symbol manipulation digital circuits |
|
Description |
Symbolic simulation is an important technique used informal property verification and test generation for digital circuits. Existing symbolic simulators predominantly operate at the gate level, reasoning about individual bits and signals. As a result, their performance does not scale well to large circuits like microprocessors. Word-level symbolic simulators address this problem to some extent, but present other challenges, such as fixpoint detection when simulating multiple modules that mutually trigger each other. In this paper, we present some exploratory ideas for performing word-level symbolic simulation over a Verilog RTL description of a circuit. We outline the basic technique of simulation and of handling fixpoints, discuss issues faced in our approach and present solution techniques to counter these issues. We also present initial experimental results obtained by applying our algorithms to a Verilog model of an x86 processor design.
|
|
Publisher |
IEEE
|
|
Date |
2009-05-20T09:07:22Z
2011-11-28T08:07:09Z 2011-12-15T09:57:28Z 2009-05-20T09:07:22Z 2011-11-28T08:07:09Z 2011-12-15T09:57:28Z 2007 |
|
Type |
Article
|
|
Identifier |
Proceedings of the Eighth International Workshop on Microprocessor Test and Verification, Austin, Texas, USA, 5-6 December 2007, 51-59
978-0-7695-3241-7 10.1109/MTV.2007.13 http://hdl.handle.net/10054/1391 http://dspace.library.iitb.ac.in/xmlui/handle/10054/1391 |
|
Language |
en
|
|