Skip to content
STIMSMITH

blackbox ALU

Concept WIKI v1 · 8/1/2026

In the riscv-formal verification framework, the 'blackbox ALU' feature (controlled by the `RISCV_FORMAL_BLACKBOX_ALU` macro) allows the actual ALU operations of a core under test to be abstracted away when checking the consistency of the stream of retired instructions (e.g., the 'regcheck' check), so that the formal tool does not need to reason about ALU internals to validate instruction-stream behavior.

Overview

blackbox ALU is a configuration option of the riscv-formal framework. It instructs the formal verification environment to hide (black-box) the arithmetic logic unit of the processor core under test when the goal of the check is to verify properties about the stream of retired instructions rather than the exact arithmetic results.

This is useful because reasoning about concrete ALU behavior can be a major source of complexity for the solver. By black-boxing the ALU, the formal engine only needs to establish consistency properties (for example, that retired instructions agree with the register file state) without having to prove the correctness of the ALU's internal computations.

How it is enabled

The behavior is controlled by the presence or absence of the blackbox option in the riscv-formal configuration. When enabled, the C preprocessor macro RISCV_FORMAL_BLACKBOX_ALU is defined and may be used inside the core-under-test source to conditionally hide the ALU.

When it is used

According to the riscv-formal documentation, the RISCV_FORMAL_BLACKBOX_ALU macro is intended for checks that operate on the consistency of the stream of retired instructions, such as the regcheck check. It is not meant for checks that must reason about the actual computed values produced by the ALU.

This contrasts with RISCV_FORMAL_BLACKBOX_REGS, which is used when checking for correct implementation of individual RISC-V instructions (the insncheck) and abstracts the register file instead of the ALU.

Practical implications

  • Solver simplicity. Hiding the ALU reduces the internal state the formal tool must track during instruction-stream checks.
  • Scope of verification. A black-boxed ALU check can confirm that the architectural contract of the retired instruction stream holds, without proving that the ALU computes the correct arithmetic result. To verify ALU correctness, ALU-internal checks (without RISCV_FORMAL_BLACKBOX_ALU) are required.
  • Core-side integration. The core under test must conditionally compile the ALU out (or otherwise hide it from the formal tool) whenever RISCV_FORMAL_BLACKBOX_ALU is defined.

Related configuration knobs in riscv-formal

The blackbox ALU option sits alongside other macros in the riscv-formal configuration system:

  • RISCV_FORMAL_BLACKBOX_REGS — black-boxes the register file for instruction-level checks (insncheck).
  • RISCV_FORMAL_COMPRESSED — indicates support for the RISC-V Compressed ISA.
  • RISCV_FORMAL_FAIRNESS — enables fairness guarantees needed for liveness checks.
  • RISCV_FORMAL_INSN_MODEL — names the per-instruction model module used by insn checks.
  • RISCV_FORMAL_CHECKER — names the checker module instantiated by the testbench.
  • RISCV_FORMAL_RESET_CYCLES, RISCV_FORMAL_CHECK_CYCLE, RISCV_FORMAL_TRIG_CYCLE, RISCV_FORMAL_CHANNEL_IDX — control the timing and targeting of checks.
  • RISCV_FORMAL_UNBOUNDED — signals unbounded model checking.
  • RISCV_FORMAL_ASSUME — pulls in a user-provided assume_stmts.vh of SystemVerilog assumptions.
  • CSR-related macros (RISCV_FORMAL_CSR_<name>, RISCV_FORMAL_CSRW_NAME, RISCV_FORMAL_CSRWH) for routing CSR state over RVFI.

See also

  • riscv-formal (the framework that defines and consumes the RISCV_FORMAL_BLACKBOX_ALU macro)

LINKED ENTITIES

1 links
riscv-formal USES

CITATIONS

3 sources
3 citations
[1] The `blackbox ALU` option causes the macro `RISCV_FORMAL_BLACKBOX_ALU` to be defined, and is toggled by the presence or absence of the `blackbox` configuration option in riscv-formal. Defining macros - RISC-V Formal documentation
[2] `RISCV_FORMAL_BLACKBOX_ALU` is intended for checks that verify the consistency of the stream of retired instructions, such as the `regcheck` check, not for proving concrete ALU results. Defining macros - RISC-V Formal documentation
[3] `RISCV_FORMAL_BLACKBOX_ALU` may be used inside the core under test to black-box the ALU, complementing `RISCV_FORMAL_BLACKBOX_REGS` which black-boxes the register file for `insncheck`. Defining macros - RISC-V Formal documentation