John Havlicek (Freescale, Inc.), Constraints in Hardware Verification: Some Industrial Perspectives

In this talk I will discuss the use of constraints in simulation-based and formal verification of hardware designs at Freescale Semiconductor. In this context, a constraint is an assumption of the design block about the signals provided by its environment. Constraints are written as properties in a suitable temporal logic. The basic uses of constraints are well known: as assumptions in formal verification computations, as checkers when the design block is integrated into larger design models, and for the generation of random simulation stimulus for the design block. Constrained random stimulus generation has been supported in Freescale by an internal, BDD-based constraint solving tool called SimGen. Achieving acceptable tool performance on an industrial scale has involved some interesting heuristic techniques and theoretical problems.