Example usage in hpm-test

Code is available in scy/example/hpm-test, using the NERV core and cover check from the RISCV-V formal verification framework<https://github.com/YosysHQ/riscv-formal/>.

Additional code provided in cover_stmts.vh is based on the rvfi_csrc_hpm_check.sv code. This code provides the SVA cover statements and assumptions needed to perform checking of the hardware performance monitoring (hpm) in the NERV core. More specifically, providing coverage of core reset completion, writing specified events to the hpmevent register, and reading an increasing value from the hpmcounter register.

hpm-test.scy

The hpm-test SCY code can be run using scy hpm-test.scy from the same directory.

The following sections analyse the SCY configuration file and the operations performed.

Design

The [design] section is as follows:

# read source
read -sv cover.sv wrapper.sv nerv.sv
prep -flatten -nordff -top rvfi_testbench
# remove testbench init assumption 
delete c:$assume$rvfi_testbench.sv*

The rvfi_testbench code provides an assumption that the core is reset during the initial stage of simulation. As the design will be put through the solver multiple times, and we want the state to be retained between iterations, we need to remove this assumption.

Sequence

The [sequence] section is as follows:

cover checker_inst.cp_reset_done:
    disable checker_inst.ap_noreset
    trace reset
    cover checker_inst.cp_hpmcounter
    cover checker_inst.cp_hpmevent2:
        cover checker_inst.cp_hpmcounter:
                trace hpm_event2

    cover checker_inst.cp_hpmevent3:
        cover checker_inst.cp_hpmcounter:
            enable checker_inst.ap_nowrite
            trace hpm_event3
        append -3:
            cover checker_inst.cp_hpmcounter:
                trace hpm_event3_2

This describes a hierarchy where everything follows from a core reset, cp_reset_done. Note that because our cover statements are inside the checker_inst module which is itself instantiated inside the top level rvfi_testbench, we need to use the qualified name checker_inst.cp_reset_done.