Skip to content

Latest commit

 

History

History
242 lines (164 loc) · 8.56 KB

config.md

File metadata and controls

242 lines (164 loc) · 8.56 KB
Raw

RISCV-FORMAL Configuration Macros

The riscv-formal insn models and checkers are configured using a few Verilog pre-processor macros. They must be defined bofore reading any riscv-formal verilog files. The first riscv-formal verilog file read after defining the macros must be rvfi_macros.vh.

Example configuration:

`define RISCV_FORMAL
`define RISCV_FORMAL_NRET 1
`define RISCV_FORMAL_XLEN 32
`define RISCV_FORMAL_ILEN 32
`define RISCV_FORMAL_COMPRESSED
`define RISCV_FORMAL_ALIGNED_MEM

The macros in this section must be defined by the user where relevant, while the next section includes additional macros which may be automatically generated depending on configuration. Defining RISCV_FORMAL, RISCV_FORMAL_NRET, RISCV_FORMAL_XLEN, and RISCV_FORMAL_ILEN is mandatory if genchecks.py is not being used.

RISCV_FORMAL_UMODE

This macro must be defined when the core under tests supports U-mode.

RISCV_FORMAL_SMODE

This macro must be defined when the core under tests supports S-mode.

RISCV_FORMAL_ALTOPS

This macro must be defined if the core under tests implements alternative arithmetic semantic.

RISCV_FORMAL_ALIGNED_MEM

Cores that only have hardware support for word-aligned memory access may choose to retire memory load/store operations for smaller units (half-words, bytes) word aligned with the appropiate rmask/wmask values to select the correct bytes. In this case the RISCV_FORMAL_ALIGNED_MEM macro must be defined.

RISCV_FORMAL_VALIDADDR(addr)

Set this to an expression of addr that evaluates to 1 when the given address is a valid physical address for the processor under test. If not defined this expression will always evaluate to true.

RISCV_FORMAL_VALIDHPMEVENT(event)

Set this to an expression of event that evaluates to 1 when the given event is a valid assignment for a hpmevent CSR. If not defined this expression will always evaluate to true.

RISCV_FORMAL_IOADDR(addr)

Set this to an expression of addr that evaluates to 1 when the given address belongs to an i/o memory region. If not defined this expression will always evaluate to true.

RISCV_FORMAL_WAITINSN(insn)

Set this to an expression of insn that evaluates to 1 when the given instruction is a wait instruction similar to WFI. (WFI does not need to be recognized by the expression. This is for non-standard instructions in addition to WFI.)

RISCV_FORMAL_PMA_MAP

Set this to the name of a module that takes an address as input and outputs the PMA info for that address. The exact interface of such a module is not entirely defined yet.

Testbench Macros

The following macros are all defined automatically when using genchecks.py. If tests are being performed manually without the generated framework, some of these macros may be required to be defined by the user prior to loading the testbench. Additional information may be found in the configuring check generation section of the procedure document.

RISCV_FORMAL

This macro is set whenever riscv-formal is used. It is actually never used by any of the riscv-formal Verilog files, but can be used by cores under test to enable or disable generation of the RVFI ports.

RISCV_FORMAL_NRET

The number of channels for the RVFI port (and thus the theoretical maximum number of instructions the core can retire via RVFI in one cycle). The value of this macro can be set by providing the nret option in the check config.

RISCV_FORMAL_XLEN

The width of integer registers in the ISA implemented by the core under test. Valid values are 32, 64, and 128. Only 32 is fully supported at the moment. genchecks.py will define this as 32, unless the isa string in the options contains rv64.

RISCV_FORMAL_ILEN

The maximum width of an instruction retired by the core. For cores supporting fused instructions this is the maximum length of a complete fused instruction. There is currently no way to automatically generate tests with a value other than 32.

RISCV_FORMAL_COMPRESSED

For cores supporting the RISC-V Compressed ISA this define must be set. This will be automatically defined if the c extension appears in the isa string.

RISCV_FORMAL_BLACKBOX_REGS

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.

RISCV_FORMAL_BLACKBOX_ALU

When checking for consistency of the stream of retired instructions (such as "regcheck") it is possible to black-box the actual ALU operations. This macro may be used in the core under test to black-box the ALU. Controlled by the presence or absence of the blackbox option.

RISCV_FORMAL_FAIRNESS

When checking for liveness of the core, then the peripherals and abstractions used in the check must guarantee fairness. This macro should be tested by the peripherals and abstractions to decide if fairness guarantees should be enabled. Automatically defined for liveness and hang checks.

RISCV_FORMAL_RESET_CYCLES

The number of cycles to hold reset high for at the start of the model checking.

RISCV_FORMAL_CHECK_CYCLE

The cycle number in which checks will be performed. For bounded model checking, this should be the solver depth.

RISCV_FORMAL_TRIG_CYCLE

The cycle number in which to trigger some check specific action.

RISCV_FORMAL_CHANNEL_IDX

For checks which only operate on a single channel, this macro defines which channel is being checked.

RISCV_FORMAL_CHECKER

The name of the module to be instantiated by the testbench for formal verification. e.g. rvfi_csrw_check.

RISCV_FORMAL_ASSUME

Indicates that the assume_stmts.vh file should be included in the testbench. This file is expected to contain a series of SV assumptions that the solver should make.

RISCV_FORMAL_UNBOUNDED

This macro is used to indicate that unbounded model checking is being used.

RISCV_FORMAL_CSR_

Each CSR being connected over the RVFI interface should be defined with one of these macros. Refer to the RVFI Interface Specification for CSRs for more details on how this name is used.

RISCV_FORMAL_CSRW_NAME

This macro defines the name of the CSR under test during csrw checks.

RISCV_FORMAL_CSRWH

This macro is used in the csrw checks to indicate that the current CSR consists of two registers, with the second being of the same name but appended with 'h'.

RISCV_FORMAL_INSN_MODEL

When performing insn checks, this is the name of the module for the current instruction. e.g. rvfi_insn_add.

Macros defined by rvfi_macros.vh

The Verilog file rvfi_macros.vh defines a few useful helper macros.

RVFI_WIRES, RVFI_OUTPUTS, RVFI_INPUTS, RVFI_CONN

Macros to declare wires, output ports, or input ports for all rvfi_* signals. The last macro is for creating the proper connections on module instances. This macros can be useful for routing the rvfi_* signals through the design hierarchy.

rvformal_rand_reg and rvformal_rand_const_reg

Macros for defining unconstrained signals (rvformal_rand_reg) or constant signals with an unconstrained initial value (rvformal_rand_const_reg).

Usage example:

`rvformal_rand_reg [7:0] anyseq;
`rvformal_rand_const_reg [7:0] anyconst;

For formal verification with Yosys (i.e. when YOSYS is defined), this will be converted to the following code:

rand reg [7:0] anyseq;
rand const reg [7:0] anyconst;

For simulation (i.e. when SIMULATION is defined), this will be converted to:

reg [7:0] anyseq;
reg [7:0] anyconst;

And otherwise (for use with any formal verification tool):

wire [7:0] anyseq;
reg [7:0] anyconst;