  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.
