From Formal Data Path Verification to Formal ISA Verification

Abstract

While formal verification is widely deployed for data path functions in RTL designs of processor cores, many teams still rely on simulation with random instruction generation, to verify other aspects of the Instruction-Set Architecture (ISA). This paper describes an approach to formal ISA verification, primarily targeted towards people already familiar with formal data path verification. The approach is implemented in the Synopsys ASIP Designer tool set, which has been used to create a variety of specialized processor architectures for commercial products.

Introduction

This paper deals with verifying RTL designs of processor cores against an ISA specification.
As the RTL design is eventually committed to hardware, considerable effort is spent to make
sure it always behaves in accordance with the ISA specification. One approach is through
simulation with random instruction generation to cover a large space of possible behaviors.
Another approach is through formal verification, where formal engines exhaustively explore
all possible scenarios in search of a counterexample to expected behavior.