Overview

ALU Constraint Verification describes the application of declarative, constraint-based modeling to an Arithmetic Logic Unit (ALU) design, in order to automatically generate stimulus vectors that respect the ALU's operational semantics. In the CRAVE constrained-random verification framework, the ALU is encoded as a randomized object whose fields — an opcode and two operands — are bound by conditional constraints that express valid ALU behavior for each supported operation.

CRAVE ALU Encoding (16-bit example)

The canonical illustration is the 16-bit ALU model shown in Figure 7 of the CRAVE paper. It declares an opcode op of type sc_bv<2> and two operands a and b of type sc_uint<16>. For each of the four opcode values, an implication-style constraint restricts the operand ranges or relations so that the arithmetic is well-defined (no overflow for addition, subtraction, and multiplication, and a non-zero divisor for the division-like operation):

• op == 0: 65535 >= a() + b() (overflow-free addition)
• op == 1: 65535 >= a() - b() and b() <= a() (overflow-free subtraction with a >= b)
• op == 2: 65535 >= a() * b() (overflow-free multiplication)
• op == 3: b() != 0 (non-zero divisor)

The pattern uses IF_THEN to make these constraints conditional on the opcode, allowing the same randomized object to cover all ALU operations.

Scalability Across ALU Bit Widths

The CRAVE paper reports a direct comparison of CRAVE against the SCV library for ALU widths of 4, 12, 16, 24, and 32 bits. The reported run-times (in seconds) are:

(TO denotes time-out; MO denotes memory-out.)

As the bit width grows, SCV fails to solve the ALU constraints — at ALU16 it already hits its 32-bit memory restriction (a BDD representation that must encode every solution path is required to give each solution equal probability), while CRAVE continues to scale using its SMT-based backend, generating stimuli before the BDD is ready. This contrast is the central empirical claim of the ALU experiment in CRAVE.

Verification Implications

ALU Constraint Verification in this style demonstrates that:

1. ALU semantics can be expressed compactly as conditional constraints on opcode and operands.
2. Constraint solvers vary significantly in their ability to handle wide-integer arithmetic, with BDD-based approaches exhausting memory at modest widths and SMT-based approaches remaining tractable.
3. CRAVE exposes multiple solver backends (Z3, Boolector, MiniSAT, PicoSAT, CUDD, AIGER, SWORD), enabling the ALU benchmark to be run across engines to compare performance.