Keywords

figure a
figure b

1 Introduction

Integer multipliers are crucial components in processing units. Ensuring their correctness through formal verification is essential; however, historically, verifying them has proven to be challenging [4, 6, 15, 18]. Automated methods like SAT solving, BDDs, and computer algebra systems have either failed to scale or demonstrated limited applicability in this context [2, 8, 12, 16, 25]. On the other hand, the S-C-Rewriting method has been shown to be very efficient in formally verifying a large variety of RTL designs [21, 24,25,26].

S-C-Rewriting and auxiliary programs are packaged into the VeSCMul tool (pronounced “vesk-muhl”). VeSCMul is designed to be user-friendly and comprehensive for sound, fast, and automatic verification of multiplier-centric RTL designs. It has an improved user interface tailored for non-experts, simplifying tool usage. VeSCMul has also introduced the support for fully automatic verification with its new adder detection program. VeSCMul has undergone extensive testing on thousands of public benchmarks as well as proprietary industrial designs at Intel Corporation. Its open-source and free-license status enables others to use this tool for similar verification tasks.

This paper presents VeSCMul, and it is outlined as follows. Sec. 2 walks through a demo for VeSCMul, showing the user-interface. Sec. 3 gives an overview of the tool flow. Sec. 4 lists some of the noteworthy features. Sec. 5 delivers experimental results on both public and proprietary designs. Sec. 6 discusses related work and concludes the paper.

2 Installation and a Demo

VeSCMul is implemented in the ACL2 theorem prover and programming language [10], and it is fully verified. VeSCMul is open-source with the MIT license, included as a Community Book in the ACL2 distribution on Github, which can be found at https://github.com/acl2/acl2 under books/projects/vescmul. Installing ACL2 and building the books will bring along VeSCMul.

A comprehensive and up-to-date documentation for VeSCMul is available as part of ACL2’s manual, accessible at http://acl2.org/manual. This documentation is extensive, covering thousands of topics from ACL2 sources and Community Books. Throughout this paper, various documentation topics are referenced using the notation “:doc <topic>”.

Once ACL2 is installed and books are built, users can run a VeSCMul demo by running the events from Listing 1.1 within an ACL2 interactive session.

figure c

The first event (include-book) loads VeSCMul and required libraries, which takes about a minute. Alternatively, an executable can be created for instant loading (see :doc save-exec). The second event (vescmul-parse) parses the target design, taking a few seconds. The Verilog file is available in the ACL2 git repository under the books/projects/vescmul/demo directory. The third event (vescmul-verify) uses VeSCMul to verify the design. :concl specifies the conjecture, with RESULT as the output signal name, and IN1 and IN2 as input signal names. logext sign-extends bit-vectors (represented as integers), and loghead zero-extends or, in other words, truncates them. The inputs are 64-bit signed numbers, producing a 128-bit multiplication result. VeSCMul can fully verify this design in 1-2 seconds (as tested on a Macbook M1 pro).

3 Tool Flow

The vescmul-parse and vescmul-verify utilities are two LISP macros that invoke various programs to parse and then verify target designs.

The vescmul-parse macro packs VL/SV/SVTV utilities to parse Verilog designs and create symbolic simulation vectors. These utilities are publicly available and come with the ACL2 installation. They have been developed and used in industry (i.e., Centaur Technology and Intel Corporation) (see :doc sv).

The vescmul-verify macro gathers the symbolic simulation objects, detects adder components, applies the S-C-Rewriting algorithm, and maybe utilizes SAT solving in the end. The program flow is shown in Fig. 1. These steps are explained as follows.

Fig. 1.
figure 1

Flow chart of vescmul-verify. (1) User states a conjecture with high-level specification. (2) VeSCMul receives a sea of gates from the design. (3) The tool identifies and rebuilds half/full-adders in this sea of gates. (4) The design and the spec are rewritten with the S-C-Rewriting methodology. (5) If rewriting is not conclusive, rewritten conjecture can be passed to FGL for SAT solving.

Full size image

(1) Specification is provided by the user, stating a relation between input and output signals. This is typically a combination of multiplication (*), addition (+), subtraction (-), truncation/zero-extension (loghead), sign-extension (logext), part selection (part-select), and possibly user-defined functions.

(2)(3) S-C-Rewriting algorithm needs to differentiate and specially rewrite adder components (e.g., full/half-adders) in a design. In previous work [25, 26], S-C-Rewriting algorithm was used only for designs whose design hierarchy information around adders was readily available. VeSCMul has been improved to now support flattened designs. This is achieved by an internal program that goes through a sea of gates to identify and mark the adder components before applying the S-C-Rewriting algorithm. Tests have shown that this program works very well for successful verification of various architectures (see Sec. 5). Should the program not identify some adders and the verification attempt fails because of that, users may also pass hierarchical verification hints (see :doc vescmul).

(4) When VeSCMul applies S-C-Rewriting, the rewriter tries to rewrite both the specification and the design to the same form (i.e., s-c-form [25]), and the two sides are compared syntactically. For correct multiplier designs, this is usually enough to prove the conjecture.

(5) If S-C-Rewriting cannot show the conjecture to be correct, it returns its rewritten form. Users have the option to automatically use the FGL utility [19] (see :doc fgl) that can bit-blast the rewritten conjecture, perform AIG transformations, and invoke an external SAT solver like CaDiCaL [1]. FGL is also a verified program. This can either generate counterexamples for false conjectures, or help finalize the proofs in some fringe cases. For example, in x86 multiplier designs, extra circuitry is used to calculate flags based on multiplication results, such as the overflow flag that is set when a certain portion of the result are not homogeneously 0s or 1s. VeSCMul by itself may not be able to process the extra flag logic; however, it can rewrite and simplify the multiplication component, send the rewritten expression to an external SAT solver through FGL, and finalize such proofs in a matter of seconds or minutes. Note that if the multiplication component is not rewritten as intended by S-C-Rewriting, it is unlikely for a SAT solver to scale and finish the proofs for operand sizes greater than 16-bits.

4 Notable Features and Compatible Tools

This section highlights some of the useful and noteworthy features of VeSCMul as well as compatible tools.

Customizable specification: Users can state their own specifications to verify various multiplier configurations such as multiply-add, dot product, and multipliers with shifted, truncated and/or saturated outputs.

Automatic adder detection: VeSCMul includes an adder-detection program that identifies and marks adders before employing the S-C-Rewriting algorithm. This makes the overall verification procedure fully automatic for a large variety of multiplier designs (see Sec. 5 for experiments).

End-to-end verified: The author has rigorously verified, using ACL2, that VeSCMul’s all rewriting operations on given conjectures are sound. Users can place high confidence in the results when a design is claimed to be correct. Verifying such a substantial program is a complex process, demanding ACL2 expertise [20,21,22].

Exporting a clean multiplier with design hierarchy: The included adder-detection program can be used as a stand-alone feature. Given a flattened multiplier design, VeSCMul can export a functionally equivalent Verilog module with adder components separated as half/full-adder submodules. This feature may be particularly useful for researchers addressing the multiplier verification problem, where adder detection can be a common challenge [7, 11, 12, 14]. For soundness, VeSCMul includes a mechanism for formal equivalence checking between the original and exported designs.

Integration into other verification flows: Proofs generated by VeSCMul can be integrated into other ACL2-based verification workflows. For instance, when verifying floating-point fused-multiply-add (FMA) operations, which often involves decomposing the design into integer multiplication and post-multiplica-tion parts, VeSCMul can be used for the multiplication part while SAT solving can be employed for the rest. Existing and actively used decomposition tool flows in ACL2 (see :doc decomposition-proofs) and VeSCMul are compatible.

Verification of sequential circuits: VeSCMul can handle sequential circuits, including pipelined designs. Additional key arguments can be provided to vescmul-parse to verify such designs (see :doc vescmul-parse). Modules with control logic reusing the same circuitry for various arithmetic operations (e.g., see :doc multiplier-verification-demo-2) are also supported.

Waveform generation: VeSCMul is compatible with another tool (see :doc svtv-debug$) for generating waveforms in the VCD format. This capability can be valuable for pinpointing the cause of bugs in case of counterexamples.

5 Experiments

VeSCMul has undergone extensive testing and utilization across various architectures in both public benchmarks and proprietary x86 processor design projects at Centaur Technology and Intel Corporation.

Various benchmarks are gathered for experiments using publicly available generators  [3, 13, 23]Footnote 1 Summation trees include Dadda (dt), Wallace (wt), 4-to-2 compressor (4:2), array (ar), redundant binary addition (rbat), balanced delay (bdt), overturned stairs (os) trees. Partial products include signed/unsigned (s/u) simple (sp), Booth radix-2 (b2), radix-4 (r4), radix-8 (r8), radix-16 (r16) encodings. Final stage adders include block carry lookahead (bcla), carry lookahead (cla), carry-select (csel), Ladner-Fischer (lf), carry-skip (csk), conditional sum (cond), Brent-Kung (bk), ripple-carry (rp), Kogge-Stone (ks), Han-Carlson (hc), J. Sklansky conditional (jsk) adders.

Table 1 contains a large number of benchmarks to compare the performance of VeSCMul to other prominent verification tools: AMulet [8] and RevSCA2 [12] that target \(n \times n\)-bit multipliers with 2n-bit results. The newest version of AMulet (AMulet2) timed out for the majority of the benchmarks; the owner is notified, and AMulet1 is used in the experiments instead. The results for AMulet1 includes the time to check for proof certificates. RevSCA2 is neither a verified program nor does it produce certificates to check its results. These experimental results show that VeSCMul scales much better for large multipliers.

Table 1. Proof-time results with success rates for a large set of nxn-bit multipliers
Full size table
Table 2. Proof-time and memory allocation for various designs
Full size table

In addition to standard input/output sizes (\(n \times n\)-bit multipliers with 2n-bit results), Table 2 includes VeSCMul’s verification results for variations such as multiply-add (e.g., \(64 \times 64 + 64\)), multipliers with asymmetric operand sizes (e.g., \(10 \times 1024\)), shifted/truncated outputs (e.g., \(64 \times 64\)[95:32] returns the output bit positions from 32 to 95), and dot product (e.g., \(8(16 \times 16)+32\) is an 8-point dot product with 16-bit operands accumulating onto a 32-bit number). Comparable verification tools do not support these configurations. VeSCMul can fully automatically verify these designs without user hints or SAT solvers.

Moreover, around 7500 different multiplier designs with diverse architectures, operand sizes, operations, truncation, and shifting were randomly generated [23]. Overall, VeSCMul achieved a 98% success rate for fully automatic verification without hints or SAT solvers. The remaining 2% is mostly made up of multipliers with a special 7-to-3 compressor tree, and shifted multipliers, but they could still be verified by VeSCMul with a user-provided design hierarchy hint.

VeSCMul has also proven successful in industrial designs, particularly for Intel x86 instructions with various functional configurations, including multiply-accumulate, dot product, output shifting/truncation, flag calculations based on multiplication results, and saturation. In some cases, the assistance of a SAT solver becomes necessary (for flags and saturation). These designs can be fully verified rapidly and automatically, with results similar to those in the public designs. To the best of the author’s knowledge, VeSCMul is the first tool to achieve comparable verification tasks scalably and automatically.

Additionally, VeSCMul has played a vital role in the verification flow of floating-point multiply and fused-multiply-add operations. Verifying these designs is notably challenging, with no known fully automated verification method. We employ decomposition techniques [5, 17], where VeSCMul is used for the multiplication part, significantly reducing manual effort. Complete verification of single and double precision operations can be completed in under an hour.

6 Related Work and Conclusion

AMulet [8], RevSCA2 [12], and DyPoSUB [14] are other state-of-the-art tools for multiplier verification. Like VeSCMul, AMulet prioritizes soundness and can produce proof certificates. In contrast, RevSCA2 and DyPoSUB lack such proofs or mechanisms, and DyPoSUB has been identified as unsound [9]. Additionally, these tools primarily focus on verifying \(n\times n\)-bit multipliers with 2n-bit results. On the other hand, VeSCMul stands out by offering scalable and automatic verification for a broader range of multiplier-centric arithmetic circuits, and it allows users to specify their conjectures. These target designs can encompass regular multipliers, multiply-add operations, dot products, and operations involving shifting, truncation, accumulation, and saturation.

This paper has showcased VeSCMul for multiplier verification, which has demonstrated favorable results in experiments involving both public and proprietary RTL designs. This tool is open-source and compatible with other hardware verification tools. It has an improved user-interface tailored for ACL2 novices. The tool itself is fully verified, so users can have a high level of confidence in its soundness. Future work includes adding support for more input formats (currently limited to System Verilog) such as AIGER and DIMACS CNF, and further enhancements in automation to handle corner-case designs that currently require user hints for verification.