Testing Sentinel

Todo

As is custom, although public and documented, the DoIt tasks should be considered unstable; pdm run [any-script-besides-doit] should be preferred. Any advice to use doit directly on this page is because “I haven’t made the ergonomics better yet”.

Sentinel tests are divided into four categories, under the test directory at the root:

Name/Path	Description	Depends On (Nonexhaustive)
sim	Bespoke simple tests	pytest, Simulator
upstream	RISC-V unit tests maintained upstream	pytest, Simulator
formal	RISC-V Formal test suite	riscv-formal, sby, yosys, boolector
riscof	Tests against RISC-V specification	riscof, sail-riscv, Simulator

Tests categories are roughly ordered in finding the most egregious bugs quickly before spending more computing effort on more subtle bugs. E.g. if a sim test fails, there is definitely something very wrong such that no other test suite is likely to pass. sim, upstream, and a single riscof test are likely to fail quickly if there’s something wrong, while formal and the full riscof suite will take longer, especially on more subtle bugs not found by sim and upstream.

Prerequisites

Before running tests, make sure all submodules are checked out:

git clone --recurse-submodules https://codeberg.org/cr1901/sentinel

or

git clone https://codeberg.org/cr1901/sentinel
cd sentinel
git submodule update --init --recursive

While I split the dependencies in the table above, I assume for testing you’ll be focusing on all categories. To that end, make sure pytest, doit, Verilog_VCD, riscof (Linux only), sby, riscv64-unknown-elf-gcc, boolector, and yosys are installed. The first five can be installed using the following:

pdm install -G dev [riscof]

See here for hints on how to get sby, riscv64-unknown-elf-gcc yosys, and boolector. The WASM versions are not supported for testing at this time.

Sim And Upstream

Note

Nominally, I’d want doc tests to also be controlled by pytest, using pytest-sphinx. However, I can’t get it to work consistently. In the interim, use pdm doc-test instead.

sim and upstream tests can be run using the same commands:

pdm test [-k ...] [--vcds]

or

pdm test-quick [-k ...] [--vcds]

If the --vcds option is provided, pytest will create a VCD file with the same name as the test(s) at the Sentinel repo root, regardless of whether the test(s) failed or not.

sim and upstream tests are very similar, in that they both are driven by pytest and use an overlapping set of fixtures. pytest in turn drives Amaranth’s Simulator via the pytest-amaranth-sim plugin.

Diferences between sim and upstream tests include:

• sim tests are handcrafted assembly strings using bronzebeard.

• upstream tests are raw binary files assembled from the riscv-tests repo binaries.

• In the upstream tests, a fixture waits for each binary to either time out, or write a value to a specific address. The test fails if the test times out (65536 clocks), or the value written is not expected.

• sim tests, on the other hand, will use its own fixtures to run single (or batches of) instructions before pausing. During each pause, the simulation state is compared to a hand-calculated expected state; the test fails if they don’t match.

Right now (11/5/2023), the difference between test and test-quick is minimal; both commands run sim and upstream tests.

While tests are run via pytest, the riscv-tests binaries are generated using the dodo.py at the root of this repo. If you need to regenerate binaries, assuming riscv64-unknown-elf-gcc is installed and on the path already, use pdm run compile-upstream. This will also check out the submodule and for you.

RISC-V Formal

The RISC-V Formal Framework defines a Verilog wrapper over RISC-V designs, along with a large set of Verilog code. The Verilog code contains asserts, which indicate properties that a compliant RISC-V implementation should satisfy. With additional tooling (that RISC-V Formal can invoke), it is possible to test that these properties hold across time (clock cycles) from an initial state, using a technique called Bounded Model Checking (BMC).

In short, BMC tests that assertions hold by intelligently trying every combination of inputs during every clock cycle. It’s not known whether BMC/SAT solving is always faster than a worst-case brute-force search, but in practice there’s a speedup for real world problems. Testing Sentinel with RISC-V Formal is no exception.

Read This First!

Before hacking the formal tests, I suggest reading the Procedure and Config sections of the RISC-V Formal docs to get a feel, as they complement each other. The Procedure describes the format of checks.cfg, while the Config section list some Verilog macros available to the Verilog wrapper and checks.cfg. Looking at the quickstart, and the configs for PicoRV32 and SERV also helped me greatly :D. Most in-tree cores seem to follow the same file structure; I follow suit, but ignore the generated Makefile from genchecks.py.

I’m not sure if this is all documented in one place, but the overall flow of RISC-V Formal is something like this:

• genchecks.py reads checks.cfg and generates Verilog and config (cfg) files for SymbiYosys/sby. It also copies your CPU and wrapper Verilog files to a place that sby can find it, and provides a Makefile for invoking sby.

  sby is a driver program that automates common verification tasks based on cfg files. It is very doable to go without sby for your own verification flow. However, RISC-V Formal uses sby, and there’s no real advantage for me to bypass it using doit.

• sby calls yosys to convert the all the Verilog code emitted/copied by genchecks.py into a description of your circuit in a standardized format for SMT solvers.

• sby then calls yosys-smtbmc (provided with yosys), which annotates the SMTv2 file(s) in the previous step to create an SMT problem that corresponds to BMC, as described above.

• yosys-smtbmc calls boolector, an SMT solver, and waits for the solver to determine whether your design passes BMC.

• Once boolector finishes, yosys-smtbmc will interpret from boolector and construct various files describing the results, including VCDs. They are written to paths managed by sby.

• Optionally, call disasm.py to generate disassemblies from VCDs managed by sby.

Yes, there are a number of dependencies for running RISC-V Formal programs :).

The following sections up to RISCOF (exclusive) assume some familiarity with the above docs and the RISC-V Formal flow.

Run RISC-V Formal Flow

To run the RISC-V Formal from the Sentinel repo:

pdm rvformal-all [-n num_cores]

Note

doit does not provide parallel task synchronization when -n is used. I have a workaround in the rvformal-all script to call doit run_sby:setup and force serialization until all files are generated. Please do not remove it :).

Alternatively, to run a single test, useful for when a single test is failing:

pdm rvformal test-name

You can run rvformal-status test-name or rvformal-status-all to query whether a check whether a previously-run check has succeeded or failed. This will run the test if it has not been run yet.

When I originally wrote the dodo.py, I had the need to rerun RISC-V Formal tasks that succeeded without the inputs having meaningully changed (doit by default checks file hashes, not timestamps). I unfortunately don’t quite remember the context, nor whether I fixed this issue or not. But just in case, you can run rvformal-force test-name to force-run a test and ignore dependency info. Alternatively, pdm doit forget run_sby can reset the dependency logic for all checks.

How This Repo Invokes RISC-V Formal

Right now, I don’t want to commit any specific version of Sentinel to RISC-V Formal, so I maintain its RISC-V Formal config files in this repo under tests/formal. These include:

• checks.cfg- RISC-V Formal config file passed to genchecks.py, which actually generates the tests.

• wrapper.sv- RISC-V Formal wrapper that wraps the generated Verilog of sentinel_cpu.formal.FormalTop.

• disasm.py- Create a disassembly from a VCD file of a failing test. Not actually used by RISC-V Formal itself, but every other core has it :). Mine is slightly modified to play nice with doit’s parallel tasks (generate unique filenames).

The rvformal and rvformal-all pdm scripts perform some housekeeping such as generating Sentinel’s Verilog code and copying the above files into the riscv-formal source tree at cores/sentinel; as explicitly stated by RISC-V Formal’s README.md:

Out of tree generation with genchecks.py is not currently supported.

genchecks.py in turn creates many SymbiYosys/sby config files and a Makefile in cores/sentinel/checks at the riscv-formal root. The generated Makefile is not complicated; it simply invokes sby [check_cfg_file] for each available check, and so I elect to use pdm/doit to run checks.

If doit finds any VCD files in cores/sentinel/checks after a test, which usually, but not always (e.g. cover) indicates a failed check, doit will copy the VCD to the Sentinel repo root. Additionally, doit will invoke disasm.py to create a disassembly that corresponds to the RISC-V instructions found in the VCD file. The disassembly and VCD files will have the same name as the check, but with .s and .vcd extensions respectively.

The following checks, derived from the sby config file names (they correspond to sections in Procedure nicely enough), are available:

Note

This list should reflect the SBY_TESTS tuple in dodo.py. It may occassionally be out of date.

• causal_ch0

• cover

• insn_addi_ch0

• insn_add_ch0

• insn_andi_ch0

• insn_and_ch0

• insn_auipc_ch0

• insn_beq_ch0

• insn_bgeu_ch0

• insn_bge_ch0

• insn_bltu_ch0

• insn_blt_ch0

• insn_bne_ch0

• insn_jalr_ch0

• insn_jal_ch0

• insn_lbu_ch0

• insn_lb_ch0

• insn_lhu_ch0

• insn_lh_ch0

• insn_lui_ch0

• insn_lw_ch0

• insn_ori_ch0

• insn_or_ch0

• insn_sb_ch0

• insn_sh_ch0

• insn_slli_ch0

• insn_sll_ch0

• insn_sltiu_ch0

• insn_slti_ch0

• insn_sltu_ch0

• insn_slt_ch0

• insn_srai_ch0

• insn_sra_ch0

• insn_srli_ch0

• insn_srl_ch0

• insn_sub_ch0

• insn_sw_ch0

• insn_xori_ch0

• insn_xor_ch0

• pc_bwd_ch0

• pc_fwd_ch0

• reg_ch0

• unique_ch0

• liveness_ch0

• csrw_mscratch_ch0

• csrc_any_mscratch_ch0

• csrw_mcause_ch0

• csrw_mip_ch0

• csrc_zero_mip_ch0

• csrw_mie_ch0

• csrc_zero_mie_ch0

• csrw_mstatus_ch0

• csrc_const_mstatus_ch0

• csrw_mtvec_ch0

• csrc_zero_mtvec_ch0

• csrw_mepc_ch0

• csrc_zero_mepc_ch0

• csrw_mvendorid_ch0

• csrc_zero_mvendorid_ch0

• csrw_marchid_ch0

• csrc_zero_marchid_ch0

• csrw_mimpid_ch0

• csrc_zero_mimpid_ch0

• csrw_mhartid_ch0

• csrc_zero_mhartid_ch0

• csrw_mconfigptr_ch0

• csrc_zero_mconfigptr_ch0

• csrw_misa_ch0

• csrc_zero_misa_ch0

• csrw_mstatush_ch0

• csrc_zero_mstatush_ch0

• csrw_mcountinhibit_ch0

• csrc_zero_mcountinhibit_ch0

• csrw_mtval_ch0

• csrc_zero_mtval_ch0

• csrw_mcycle_ch0

• csrc_zero_mcycle_ch0

• csrw_minstret_ch0

• csrc_zero_minstret_ch0

• csrw_mhpmcounter3_ch0

• csrc_zero_mhpmcounter3_ch0

• csrw_mhpmevent3_ch0

• csrc_zero_mhpmevent3_ch0

• csr_ill_eff_ch0

• csr_ill_302_ch0

• csr_ill_303_ch0

• csr_ill_306_ch0

• csr_ill_34a_ch0

• csr_ill_34b_ch0

• csr_ill_30a_ch0

• csr_ill_31a_ch0

Sentinel Formal Top-Level Module

Components for interfacing Sentinel to external verification tools.

class sentinel_cpu.formal.FormalTop(*args, src_loc_at=0, **kwargs)

Sentinel CPU RVFI Harness.

Todo

As mentioned previously, FormalTop does not connect to the rest of Sentinel via a well-defined interface.

It relies directly on many sentinel_cpu.top.Top internal signals that I would rather be exposed via an Interface, but progress has been slow. This includes hardcoding microcode addresses constants as class attributes.

I’m deferring describing how this module works internally until I clean it up. Fortunately, I don’t think it’s not exceptionally difficult to follow in its current state. Cleanup mostly consists of:

• Fleshing out the aforementioned interface started in sentinel_cpu.top.Top.rvfi.

• Refactoring the implicit state machine from the combination of in_init, committed_to_insn, and just_committed_to_insn into an explicit one.

bus

A forwarded copy of sentinel_cpu.top.Top.bus.

Type:

Out(wishbone.Signature)

irq

A forwarded copy of sentinel_cpu.top.Top.irq.

Type:

In(1)

rvfi

Signature Member implementing the RISC-V Formal Interface.

When exported to Verilog, Amaranth will generate its own names for ports, and the won’t necessarily match the RISC-V Formal Interface names in the linked document. As of Amaranth 0.5.4, I use the following Verilog macros to forward the exported FormalTop port names to RISC-V Formal IP ports:

`define RVFI_AMARANTH_PORT(suff) .rvfi__``suff(rvfi_``suff)
`define RVFI_CSR_AMARANTH_PORTS(csr) \
    .rvfi__csr__``csr``__rmask(rvfi_csr_``csr``_rmask),       \
    .rvfi__csr__``csr``__wmask(rvfi_csr_``csr``_wmask),       \
    .rvfi__csr__``csr``__rdata(rvfi_csr_``csr``_rdata),       \
    .rvfi__csr__``csr``__wdata(rvfi_csr_``csr``_wdata)

Its Signature looks like the following:

Todo

Fix goofy formatting, currently (1/11/2025) a side-effect of how NORMALIZE_WHITESPACE in doctest works.

Signature({'valid': Out(1),
    'order': Out(64),
    'insn': Out(32),
    'trap': Out(1),
    'halt': Out(1),
    'intr': Out(1),
    'mode': Out(2),
    'ixl': Out(2),
    'rs1_addr': Out(5),
    'rs2_addr': Out(5),
    'rs1_rdata': Out(32),
    'rs2_rdata': Out(32),
    'rd_addr': Out(5),
    'rd_wdata': Out(32),
    'pc_rdata': Out(32),
    'pc_wdata': Out(32),
    'mem_addr': Out(32),
    'mem_rmask': Out(4),
    'mem_wmask': Out(4),
    'mem_rdata': Out(32),
    'mem_wdata': Out(32),
    'csr': Out(Signature({'mscratch': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mcause': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mip': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mie': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mstatus': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mtvec': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mepc': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'misa': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mvendorid': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'marchid': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mimpid': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mhartid': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mconfigptr': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mstatush': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mcountinhibit': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mtval': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)})),
        'mcycle': Out(Signature({'rmask': Out(64),
            'wmask': Out(64),
            'rdata': Out(64),
            'wdata': Out(64)})),
        'minstret': Out(Signature({'rmask': Out(64),
            'wmask': Out(64),
            'rdata': Out(64),
            'wdata': Out(64)})),
        'mhpmcounter3': Out(Signature({'rmask': Out(64),
            'wmask': Out(64),
            'rdata': Out(64),
            'wdata': Out(64)})),
        'mhpmevent3': Out(Signature({'rmask': Out(32),
            'wmask': Out(32),
            'rdata': Out(32),
            'wdata': Out(32)}))}))})

Type:

Out(Signature)

elaborate(plat)

RISCOF

RISCOF, the RISC-V Compatibility Framework, is the test suite that RISC-V International requires implementations to pass as part of approval for licensing trademarks, etc. I don’t plan to get involved in that stuff right now, but it’s nice to be prepared with evidence such that I can say “Here is Sentinel passing your tests. Now I can say it implements RISC-V!”

Compared to RISC-V Formal, RISCOF is not comprehensive, and the docs say as much:

Passing the RISC-V Architectural Tests does not mean that the design complies with the RISC-V Architecture. These are only a basic set of tests checking important aspects of the specification without focusing on details.

The RISC-V Architectural Tests are not a substitute for rigorous design verification.

However, RISCOF tests are tested against the software version of the RISC-V specification itself, the SAIL-RISCV Golden Model. AFAICT, the RISCOF tests are based on the riscv-tests I use for the upstream category, but modified to support testing against the SAIL model.

While RISC-V Formal is a well-designed test suite that has helped me find a number of legitimate bugs, and tests more comprehensively than RISCOF, it is, AFAIK, an alternate software implementation of the RISC-V specification. Although unlikely, it is possible in theory for all tests in other categories to pass while RISCOF tests fail. Such a failure would indicate something particularly subtle is wrong, including (in somewhat order of most to least likely):

• Sentinel CPU

• My RISCOF plugin :)

• My other tests

• RISC-V Formal

• RISCOF/SAIL-RISCV/The specification itself

Even if the bug is ultimately in my code, a particularly subtle bug would require me to talk to other people more directly involved in formalizing the RISC-V spec to get feedback and advice.

In short, I include RISCOF tests to show that “Sentinel passes the tests that RISC-V International expects an implementation to pass”. If they fail, they can also help me find bugs in my code as well as others :).

Run RISCOF Flow

Todo

At present, RISCOF tests presently require Linux to run because I had trouble installing an OCaml toolchain on Windows at the time. In addition, I recall a few *nix-isms in the RISCOF Python package. I will fix this in the future.

Running RISCOF is orchestrated by the dodo.py at the root of this repo. To check out the RISCOF submodule and run the flow, run:

pdm run riscof-all

The above will:

• Check out the RISCOF submodule for you.

• Decompress the SAIL emulator, if necessary.

• Generate a riscof_work directory full of config files and tests for you using riscof testfile, subject to DoIt’s dependency management.

• Delete a number of output subdirectories (dut and ref) under riscof_work; riscof expects these to be empty before running a test. This will not fail if the various dut and ref directories don’t exist.

• Finally, run RISCOF flow using riscof run.

The results of riscof run will be available under riscof_work/report.html, and the various dut and ref subdirectories provided for each test under rv32i_m (ELF files, disassemblies, etc).

One of the files generated in riscof_work will be a test_list.yaml. Occassionally, it may be useful to truncate the test_list.yaml to run a subset of generated tests. Since RISCOF currently (as of 11/11/2023) doesn’t make running individual tests easy, use the following:

pdm run riscof-override /path/to/new/test_list.yaml

Note that if the “delete a number of subdirectories” step needs to run, all dut and ref subdirectories possibly containing interesting results will be deleted! In addition, checking whether test_list.yaml is up-to-date is hash based; two separate test_list.yaml files with the same exact contents will be considered the same file to riscof-override.

How This Repo Integrates RISCOF

RISCOF requires several inputs to run. Although you must have an existing SAIL binary, RISCOF takes care of installing a SAIL plugin and config.ini for you. Like in SERV, the SAIL (and Sentinel) plugins have been modified to expect riscv64-unknown-elf-gcc, even for 32-bit, but otherwise need not be modified further. Additionally, config.ini is set up properly and should also be a pretty static file.

The required sail-riscv and riscv-arch-test repos are provided as submodules for convenience. It’s not clear to me that RISCOF depends on any particular version of these repos. I haven’t tried it yet, but it should be safe to update these submodules independently of the rest of RISCOF.

Updating submodules notwithstanding, it seems to me outside of a full upgrade of RISCOF (not exposed by pdm scripts or doit), RISCOF input files are mostly static. Test development focuses on modifying files in the sentinel directory. I’ve mostly left RISCOF alone after getting it working; as I upgrade RISCOF and submodules, I’ll update these docs based on my experiences.

The sentinel directory implements the DUT plugin for Sentinel. The files contained within are explained in Model Plugin Directories. Similar the the upstream tests, the Sentinel plugin wraps the Amaranth Simulator. In fact, several pieces of code (which form the basis of pytest fixtures) are imported from the top-level test directory into the plugin! The main functional differences from upstream tests are:

• A different set of binaries are used for the plugin.

• Instead of searching for a value written to a specific address, the plugin dumps its memory state to a file after a write to a specific address. RISCOF itself uses these files to compare Sentinel’s behavior to the SAIL model.

All this setup is summarized in Running RISCV-ARCH-TESTS, with the following caveat:

• Step 2 of Section 7.1 of the RISCOF docs seems incorrect; riscof will set up the sail_cSim plugin for you as part of riscof setup --dutname=sentinel (although this step should not be necessary to run normally, and is currently not provided even in dodo.py).

Rebuilding the SAIL Golden Model

Building the SAIL RISC-V Model is tough. It requires an OCaml toolchain, and even after getting an environment set up, the C code that OCaml generates takes 30+ minutes to compile with LTO. I didn’t want to go through this again, so I include a precompiled gzipped Linux binary at riscof/bin/riscv_sim_RV32.gz. pdm riscof-all, pdm riscof-override, and doit know how to gunzip the binary on demand.

The SAIL RISC-V emulators are written in a mix of C, OCaml and the sail DSL. From a packaging standpoint, the SAIL RISC-V emulators are OCaml packages whose dependencies are described using the opam package manager and opam files. On Ubuntu 20.04, installing the prerequisites for the emulators looks something like this:

sudo apt-get install opam  build-essential libgmp-dev z3 pkg-config zlib1g-dev
opam init -y --disable-sandboxing
opam switch create create ocaml-base-compiler.4.08.1
opam install sail -y

Then, to actually (re)build the SAIL RISC-V emulators in a hopefully turnkey fashion, run pdm doit _build_sail. As with other doit tasks, this should not be relied upon for normal development. Note that the actual build requires make; opam only handles installing dependencies, and delegates to make for building.

Hint

You will probably want to run pdm doit forget _decompress_sail afterwards, so that your fresh new SAIL emulator replaces the old one :).

Todo

It’d be nice to remove the immediate dependency on make. Since we don’t want to install the emulators in the system, it should be in principle possible to cd sail-riscv, do opam install . --deps-only, and then build SAIL manually. However, I couldn’t get that to work…

Additionally, the default RISCOF SAIL plugin uses make, and I haven’t gotten around to ripping that out yet :).

As of 11/6/2023, the build instructions provided by RISCOF documentation for the SAIL RISC-V emulators are out-of-date; I didn’t successfully compile the emulator until I did opam switch create ocaml-base-compiler.4.08.1.