Title :
Supporting sequential assumptions in hybrid verification
Author :
Cerny, E. ; Dsouza, Ashvin ; Harer, Kevin ; Ho, Pei-Hsin ; Ma, Tony
Author_Institution :
Synopsys Inc., USA
Abstract :
We present a method for using a set of temporal properties (SVA, PSL, OVA, RTL monitors) as environment models for industrial-strength hybrid verification that combines formal methods with constrained random simulation. We demonstrate the effectiveness of the method on real-world designs.
Keywords :
formal specification; formal verification; OVA monitors; PSL monitors; RTL monitors; SVA monitors; formal methods; hybrid verification; random simulation; sequential assumptions; Automata; Clocks; Design methodology; Formal verification; Hardware design languages; Law; Legal factors; Signal design; Signal generators; Testing;
Conference_Titel :
Design Automation Conference, 2005. Proceedings of the ASP-DAC 2005. Asia and South Pacific
Print_ISBN :
0-7803-8736-8
DOI :
10.1109/ASPDAC.2005.1466517
