TIUP: Effective Processor Verification with Tautology-Induced Universal Properties
Yufeng Li, Yiwei Ci, Qiusong Yang
TL;DR
This paper tackles the challenge of formal processor verification by moving beyond a single self-consistency universal property to a suite of tautology-induced universal properties (TIUP). It introduces seeds from first-order tautologies to cover data paths and simple control, and constructs ISA-independent abstract specifications via template synthesis. These tautologies are mapped to an intermediate representation and then to symbolic instruction sequences through a scheduler, which is integrated with the RTL for model checking. Compared to existing universal-property methods like SQED and S^2QED, TIUP reduces false positives and scales better by decomposing verification into multiple properties, demonstrated on both in-order and out-of-order RISCV processors. The approach enables end-to-end processor verification at the architectural level and shows practical effectiveness, with future work aimed at expanding the universal-property set to cover additional anomalies.
Abstract
Design verification is a complex and costly task, especially for large and intricate processor projects. Formal verification techniques provide advantages by thoroughly examining design behaviors, but they require extensive labor and expertise in property formulation. Recent research focuses on verifying designs using the self-consistency universal property, reducing verification difficulty as it is design-independent. However, the single self-consistency property faces false positives and scalability issues due to exponential state space growth. To tackle these challenges, this paper introduces TIUP, a technique using tautologies as universal properties. We show how TIUP effectively uses tautologies as abstract specifications, covering processor data and control paths. TIUP simplifies and streamlines verification for engineers, enabling efficient formal processor verification.