Sciweavers

CAV
2008
Springer

Application of Formal Word-Level Analysis to Constrained Random Simulation

13 years 5 months ago
Application of Formal Word-Level Analysis to Constrained Random Simulation
Abstract. Constrained random simulation is supported by constraint solvers integrated within simulators. These constraint solvers need to be fast and memory efficient to maintain simulation performance. Binary Decision Diagrams (BDDs) have been successfully applied to represent constraints in this context. However, BDDs are vulnerable to size explosions depending on the constraints they are representing and the number of Boolean variables appearing in them. In this paper, we present a word-level analysis tool DomRed to reduce the number of Boolean variables required to represent constraints by reducing the domain of constraint variables. DomRed employs static analysis techniques to obtain these reductions. We present experimental results to illustrate the impact of this tool.
Hyondeuk Kim, HoonSang Jin, Kavita Ravi, Petr Spac
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CAV
Authors Hyondeuk Kim, HoonSang Jin, Kavita Ravi, Petr Spacek, John Pierce, Robert P. Kurshan, Fabio Somenzi
Comments (0)