System-Level Verification of Register-Transfer-Level Designs

Abstract

Verification has become the dominant cost in the design of hardware, often accounting for up to 70% of total design costs. One of the major challenges in the area is system-level verification of Register Transfer Level (RTL) designs. System-level verification involves proving theorems that capture the correctness of system components as a whole, not just proving isolated properties. In this talk, I will present several methods that we have developed for automatically reasoning about RTL designs. This includes:

- a sound and complete compositional reasoning framework based on refinement,

- an algorithm for solving quantifier-free formulas over the extensional theory of fixed-size bit-vectors and fixed-size bit-vector arrays (memories) that incorporates term-rewriting techniques, and

- an algorithm for converting Boolean circuits to conjunctive normal form.

These algorithms have been implemented in BAT, the Bit-level Analysis Tool. Using BAT we can prove that a 32-bit 5-stage pipelined machine model refines its instruction set architecture in less than 2 minutes. This is a significant improvement over what was previously possible, as competing methods cannot handle much simpler designs.