Blackbox Register File

Overview

In the context of the riscv-formal framework, a blackbox register file refers to the technique of replacing (or abstracting away) the architectural register file of a RISC-V core under test so that the formal tool no longer reasons about the concrete implementation of those registers. This is used to simplify the proof obligations that the framework imposes on the design.

How It Is Controlled

Black-boxing the register file is enabled through a preprocessor macro that the core-under-test (DUT) can test in its source code:

• RISCV_FORMAL_BLACKBOX_REGS — Defined when the user passes the blackbox option on the riscv-formal command line. The DUT may guard its register-file model with this macro so that, during an insncheck run, the solver does not see the actual register storage elements.

The documentation describes the purpose of this macro as follows: "When checking for correct implementation of the RISC-V instructions ('insncheck') it is possible to black-box the processor register file. This macro may be used in the core under test to black-box the register file. Controlled by the presence or absence of the blackbox option."

Related Black-Boxing Mechanisms

The same blackbox option also controls other related abstractions in the framework, notably:

• RISCV_FORMAL_BLACKBOX_ALU — Black-boxes the ALU operations when checking consistency of the retired-instruction stream (such as regcheck).

These two macros share the same trigger (blackbox option) but apply to different proof tasks (insncheck for the register file, regcheck for the ALU).

Tooling Relationship

The concept of a blackbox register file is a feature provided by the riscv-formal verification tool. It is enabled by the configuration options and macros documented in the riscv-formal configuration reference and used by cores being verified.

References

See the riscv-formal documentation for the complete list of configuration macros and their semantics.