Property-Based Dynamic Verification and Test

ISBN :978-94-007-1124-2Property-Based Verification has become a main stream part of industrial design flows, supported by a mature technology for the development of production quality design tools. For large systems that defeat formal verification methods, dynamic verification is called on designs directly connected to test generators and signal observers that are compiled from the properties. The quality of tests and debug efficiency are greatly improved. This chapter exposes the principles on which this verification approach is implemented in the Horus verification system. Temporal properties, written in a standard (PSL or SVA) language, are automatically translated into synthesizable IP's, using an efficient and proven correct method. Resulting monitors (for observing asserted properties) and generators (for generating constrained test vectors) are automatically connected to the design under verification by Horus, providing an instrumented design that can be simulated, emulated or synthesized. The method is illustrated on a realistic design: the conmax_ip controller