Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs

TL;DR

This paper introduces piecewise composition, a modular approach to mitigate path explosion in symbolic execution of hardware designs, significantly improving efficiency and enabling effective property verification directly on RTL Verilog.

Contribution

The paper presents a novel piecewise composition technique that leverages hardware modularity to enhance symbolic execution efficiency on RTL designs without translation.

Findings

Reduces path exploration by an order of magnitude

Decreases runtime by 97%

Finds assertion violations in open-source hardware designs

Abstract

Symbolic execution is a powerful verification tool for hardware designs, but suffers from the path explosion problem. We introduce a new approach, piecewise composition, which leverages the modular structure of hardware to transfer the work of path exploration to SMT solvers. We present a symbolic execution engine implementing the technique. The engine operates directly over register transfer level (RTL) Verilog designs without requiring translation to a netlist or software simulation. In our evaluation, piecewise composition reduces the number of paths explored by an order of magnitude and reduces the runtime by 97%. Using 84 properties from the literature we find assertion violations in 5 open-source designs including an SoC and CPU.