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.

• Type: Conference
• Year: 2008
• Where: CAV
• Authors: Hyondeuk Kim, HoonSang Jin, Kavita Ravi, Petr Spacek, John Pierce, Robert P. Kurshan, Fabio Somenzi
• Keywords: Boolean Variables, CAV 2008, Constrained Random Simulation, Constraint Solvers, Hardware