Application of Formal Word-Level Analysis toConstrained Random Simulation Tool Paper

摘要

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.