Certifying Phase Abstraction

TL;DR

This work addresses the verification of hardware model checkers by introducing a certifiable extension of phase abstraction. It formalizes a generic certificate format built from a restricted simulation relation and inductive witnesses, enabling end-to-end validation with lightweight SAT checks. The authors implement mc2, a certifying model checker, and demonstrate that the certification overhead remains small while preserving effectiveness across industrial benchmarks. The approach promises practical impact for trustworthy hardware verification and potential integration with theorem-proving environments such as Isabelle.

Abstract

Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.

Figures (8)

• Figure 1: An example of a cube lasso over the latches $l \in L = \{a, b, c, d\}$. In the example the tall rectangles represent cubes as partial assignments, i.e., the second cube from the left is $(\neg a) \wedge b \wedge d$. Phase 0 and 1 are marked on top of the cubes. As shown, duration $d=1$ and phase number $n=2$ yield a high number of useful signals for this cube lasso. Each latch $l$ is associated with a periodic pattern $\lambda_l$ on the right describing its behaviors for phase 0 and 1. If a latch is missing from a cube for a certain phase, it has no constraint thus we use the equality of the latch to itself in the signal. Latch $a$ turns out to be a simple clock delayed by one step. Latches $b$ and $d$ behave clock-like but only in phase 0. Latch $c$ always has the opposite value of latch $b$ in phase 1. Note that we could also have $\neg c$ in phase 1 of signal $\lambda_{b}$ but choosing a single representative for a set of equivalent signals is beneficial for the following simplification steps.
• Figure 2: Circuit transformation using phase abstraction.
• Figure 3: An example of a forwarded ($d=1$) and unfolded ($n=3$) circuit. The circles denote states in the original circuit ($0$ is the initial state). The rectangle are states in the unfolded circuit.
• Figure 4: Certification for (extended) phase abstraction. Base model checking is performed on circuit $C_{n+4}$, which produces a witness circuit $W_{n+2}$, that certifies $C_{n+2}, C_{n+3}, \text{ and } C_{n+4}$. We construct step-wise to obtain $W_0$, which is a certificate for the entire model checking procedure.
• Figure 5: Every fully initialized state of a 3-folded witness circuit contains 3 original states that form an unfolded state. Two consecutive 3-folded states contain either the same unfolded states or two states consecutive in the unfolded circuit.

Theorems & Definitions (39)

• definition thmcounterdefinition: Circuit
• definition thmcounterdefinition: Periodic Signal
• definition thmcounterdefinition: Unfolded circuit
• definition thmcounterdefinition: Factor circuit
• definition thmcounterdefinition: Rewrite circuit
• definition thmcounterdefinition: Reduced circuit
• definition thmcounterdefinition: Restricted Simulation
• definition thmcounterdefinition: Semantic independence
• lemma thmcounterlemma
• theorem thmcountertheorem