Automated formal verification of processors based on architectural models

• DOI: 10.5555/1998496.1998521
• Publication Date: 2010-10-20
• Authors: Ulrich Kühne; Sven Beyer; Jörg Bormann; John Barstow
• Keywords: Functional verification; Intelligent verification; Runtime Verification; Processor design; High-level verification; Microarchitecture; Verification

To keep up with the growing complexity of digital systems, high level models are used in design process. In today's processor design, a comprehensive tool chain can be built automatically from architectural or transaction models, but disregarding formal verification. We present an approach to generate complete property suite architecture description, that formally verify register transfer (RTL) implementation processor. The is by construction, i.e. exhaustive verification all functionality ensured method. It allows for efficient single pipeline processors, including several advanced features like multicycle instructions. At same time, structured reduces effort significantly compared manual presented techniques have been implemented FISACo, which demonstrated on industrial