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.

What you will learn:

• Shows a clear, practical method for verifying full ISA correctness—not just data‑path functions. Reveals real bugs found in pipelines, hazards, jumps, and interrupts—proof the method works.
• Explains how formal checks catch issues simulation misses, thanks to exhaustive exploration.
• Leverages automation in ASIP Designer to scale verification across complex architectures.