Simplifying Boolean constraint solving for random simulation-vector generation
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems(2004)
Abstract
Simulation by random vectors is meaningful only if the vectors meet certain requirements on the environment that drives the design under verification. When that environment is modeled by constraints, we face the problem of solving constraints efficiently. We present an efficient algorithm for simplifying conjunctive Boolean constraints defined over state and input variables, and apply it to constrained random simulation vector generation using binary decision diagrams (BDDs). The method works by extracting "hold-constraints" from the system of constraints. Hold-constraints are deterministic and trivially resolvable. They can be used to simplify the original constraints as well as refine the conjunctive partition. Experiments demonstrate significant reductions in the time and space required for constructing the conjunction BDDs, and the time spent in vector generation during simulation.
MoreTranslated text
Key words
certain requirement,binary decision diagram,conjunctive Boolean constraint,input variable,vector generation,conjunctive partition,random simulation-vector generation,random simulation vector generation,Simplifying Boolean constraint,efficient algorithm,conjunction BDDs,random vector
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined