FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping

TL;DR

<3-5 sentence high-level summary> Datapath verification for modern, parameterized hardware poses challenges for traditional bit-level methods. The paper introduces FORWORD, a word-level sweeping framework that combines constraint-aware, randomized simulation with selective SMT checks to identify and merge equivalent word-level subexpressions, aided by candidate reordering and filtering to reduce solver work. Key contributions include the first dedicated word-level sweeping engine for datapath verification, array-handling techniques, and a suite of heuristics that substantially reduce SMT calls. Empirical evaluation on a 511-case benchmark shows significant speedups over state-of-the-art bit-level tools, demonstrating improved scalability and adaptability to arithmetic-heavy datapaths.

Abstract

Modern circuit design process increasingly adopts high-level hardware construction languages and parameterized design methodologies to shorten development cycles and maintain high reusability, in contrast to traditional hardware description languages. Such designs often involve complex datapath with arithmetic operations, wide bit-vectors, and on-chip memories, whose scale and level of modeling often pose significant challenges to formal datapath verification. Traditional bit-level SAT sweeping techniques lack the necessary abstraction and adaptability that are required to establish equivalence at a higher level. In this paper, we propose FORWORD, a novel word-level sweeping verification engine tailored explicitly to formal datapath verification. FORWORD integrates randomized and constraint-driven word-level simulations, leveraging adaptive optimization to dynamically refine equivalent candidates identified during simulation. Experimental results demonstrate that FORWORD significantly outperforms state-of-the-art bit-level SAT sweeping engines and the monolithic SMT solving method, thanks to its enhanced capability in effectively identifying equivalent pairs. To the best of our knowledge, FORWORD is the first word-level sweeping engine explicitly designed for datapath verification, offering improved efficiency and adaptability to modern circuit designs.

Figures (6)

• Figure 1: Different circuit representations: (a) Verilog and (b) BTOR2
• Figure 2: Verification runtime in different scenarios when (a) word-level SMT solving prevails vs. (b) bit-level sweeping in Kissat is more effective
• Figure 3: An example of verifying a multi-functional unit under additional constraints
• Figure 4: Overview and details of the FORWORD flow. The left side illustrates the overall simplification pipeline: larger subgraphs are progressively replaced with equivalent smaller ones, reducing AST depth and size, thereby shrinking the solver’s problem scope. The right side details our simulation procedure: we use constraint- and heuristic-guided adaptive methods to generate stimuli, compute scores for candidate pairs, and apply a heuristic reordering policy followed by a lightweight filter so that the solver is invoked first on the most promising pairs.
• Figure 5: Performance improvement using modern heuristic techniques