NTV: Non-intrusive Trace-based Verification for RISC-V processors

Note: This is part of the Processor-CI project and uses files from other repositories. This tool is not meant to be used on its own.

NTV is a verification tool that leverages simulation and trace comparison to verify the cores. The processor under test trace is compared to the trace generated by Spike (RISC-V ISA Sim).

Usage

There are two steps: generating the traces and then comparing them.

1. First step needs the makefile(which points to files outside this repository), the ELF file, the Cocotb path to the register file and the output folder:

python3 exec_trace.py -m tmp/rvx/rvx.mk -e tmp/000_addi.elf -s tmp/rvx/ -r Processor.integer_file -o output/

2. Second step is to generate the spike trace:

python3 spike_trace.py -e tmp/000_addi.elf -o output/

3. Third Step is to generate the speculative final processor trace, with the help of the spike trace and then compare it

python3 compare_traces.py -s output/000_addi.spike.json -d output/000_addi.fragmented.json -o output/

Generating traces using the Spike fork:

It was necessary to change the spike memory map in order to execute programs starting at address 0x0. Most processors in Processor-CI have their starting address at this position. To change the map it was required to:

Change bootrom from 0x0:0xFFF to 0x1000:0x1FFF at riscv/platform.h

#define DEBUG_START 0x1000; #define DEBUG_SIZE 0x1000

Change reset vector to 0x0 at riscv/platform.h

#define DEFAULT_RSTVEC 0x00000000

Compile the assembly program with the following flags:

riscv32-unknown-elf-gcc -march=rv32i -mabi=ilp32 -nostdlib -Ttext=0x0 -o program.elf program.s`

Run this command for spike:

spike --isa=rv32i -m0x0:0x2000 --log-commits --instrcutions=100 program.elf

spike_trace.py does all the steps mentioned here.

Generating traces using the Cocotb simulation

Cocotb is a simulation tool that allows the use of Python code to interact with the RTL simulation.

exec_trace.py is the testbench to execute the programs. It has the memory model and instantiates the processor under test. The fetch interface, the register file and the memory are monitored in order to generate the execution trace.

elf_reader.py reads the ELF file and stores it in an list.

Comparing traces

The exec_trace.py testbench is not able to generate the full trace. It stores each part of the trace separately, in fragments:

{
 "comment": "Trace for 000_addi.elf on rvx",
 "fetches": [
  [0,5244307],
  [4,18],
  [8,19]
 ],
 "regfile_commits": [
  [11,5]
 ],
 "memory_accesses": [
  [60,5]
 ]
}

The generate_final_trace function in compare_traces.py uses the spike trace to generate a speculative trace. If the fragmented trace is correct, the final trace will also be. If the fragmented trace is wrong, the final trace may be unaligned or present other errors.

Here is an example of what should be in the final trace:

  {
    "pc": 0,
    "instr": 5244307,
    "target_reg": 11,
    "reg_val": 5,
    "mem_addr": null,
    "mem_val": null
  },

After the end of comparison, mismatches are shown:

Mismatch found:
Spike entry:     {'pc': 4, 'instr': 19, 'target_reg': None, 'reg_val': None, 'mem_addr': None, 'mem_val': None}
DUT entry:       {'pc': 4, 'instr': 18, 'target_reg': None, 'reg_val': None, 'mem_addr': None, 'mem_val': None}