Verifying the VeeR core

This example uses the VeeR EH1 RISC-V Core. In a new folder, run git clone https://github.com/chipsalliance/Cores-VeeR-EH1.

Note

This example requires Yosys built with Verific for parsing the input design. Ask us for an evaluation license for TabbyCAD to try this yourself.

Note

For more on the .sby file format, refer to https://yosyshq.readthedocs.io/projects/sby/en/latest/reference.html.

Loading the design

In the same directory as Cores-VeeR-EH1, run sby --init-config-file veer. This will produce a file, veer.sby with the following content:

veer.sby generated from sby --init-config-file veer

[options]
mode bmc

[engines]
smtbmc

[script]
read -formal veer.sv
prep -top top

[files]
veer.sv

Next up we need to add all of the files to veer.sby and read them into Yosys. The VeeR core comes with a handy veer.core file which lists all of the RTL source and includes needed. We’re going to make a command file called veer.f which we can read with Verific to load all of our source files together.

First, we start with the include directories. Both include files listed are in the design/include/ directory, so we can use a single +incdir+design/include. Next we want to list all of the source files: copy the list from veer.core and make sure to remove the - and any indentation at the start of each line. You should end up with something like the following:

[file veer.f]
+incdir+design/include
+incdir+snapshots/default
snapshots/default/common_defines.vh
design/include/veer_types.sv
design/lib/beh_lib.sv
design/mem.sv
design/pic_ctrl.sv
design/dma_ctrl.sv
design/ifu/ifu_aln_ctl.sv
design/ifu/ifu_compress_ctl.sv
design/ifu/ifu_ifc_ctl.sv
design/ifu/ifu_bp_ctl.sv
design/ifu/ifu_ic_mem.sv
design/ifu/ifu_mem_ctl.sv
design/ifu/ifu_iccm_mem.sv
design/ifu/ifu.sv
design/dec/dec_decode_ctl.sv
design/dec/dec_gpr_ctl.sv
design/dec/dec_ib_ctl.sv
design/dec/dec_tlu_ctl.sv
design/dec/dec_trigger.sv
design/dec/dec.sv
design/exu/exu_alu_ctl.sv
design/exu/exu_mul_ctl.sv
design/exu/exu_div_ctl.sv
design/exu/exu.sv
design/lsu/lsu.sv
design/lsu/lsu_bus_buffer.sv
design/lsu/lsu_clkdomain.sv
design/lsu/lsu_addrcheck.sv
design/lsu/lsu_lsc_ctl.sv
design/lsu/lsu_stbuf.sv
design/lsu/lsu_bus_intf.sv
design/lsu/lsu_ecc.sv
design/lsu/lsu_dccm_mem.sv
design/lsu/lsu_dccm_ctl.sv
design/lsu/lsu_trigger.sv
design/dbg/dbg.sv
design/dmi/dmi_wrapper.v
design/dmi/dmi_jtag_to_core_sync.v
design/dmi/rvjtag_tap.sv
design/lib/mem_lib.sv
design/lib/ahb_to_axi4.sv
design/lib/axi4_to_ahb.sv
design/veer.sv
design/veer_wrapper.sv

We have included two extra lines in there, one for +incdir+snapshots/default, and one for snapshots/default/common_defines.vh. The snapshots/default directory is generated by the configs/veer.config perl script and provides macro definitions which configure the VeeR core as needed. Provided perl is installed on the system, we can get Yosys to call this script for us when we run SBY. We also need to update the [script] section to read our new veer.f command file and change the top module to veer_wrapper. This gives us the following:

[script]
exec -expect-return 0 -- bash -c 'RV_ROOT=$PWD ./configs/veer.config'
read -f -formal veer.f
prep -top veer_wrapper

The perl script expects an environment variable, RV_ROOT, which defines the root location in which to generate. By using bash -c we can use the SBY output directory (accessed via $PWD) as this root location. The -f flag in the read command is passed to Verific to signal that a command file is being read.

Finally we have the [files] section:

[files]
Cores-VeeR-EH1/design
Cores-VeeR-EH1/configs
Cores-VeeR-EH1/tools

In addition to the source files in the design directory, we are also including the config script in configs, which itself references the files in the tools directory. By defining veer.f in the SBY file, we skip the need to include it in the files list.

Running SBY now we might see something like the following:

SBY [veer] prep: ERROR: CLK tck on $verific$ir_reg$design/dmi/rvjtag_tap.sv:142$7750 ($dff) from module rvjtag_tap_default also used with opposite polarity, run clk2fflogic instead.

This tells us that we have a clock signal, tck in this case, which is triggering on both positive and negative edges. This means we need to enable multiclock mode by adding multiclock on to the [options] section. At this point we can now run BMC and get our first failed counter trace. The model checker can start the design in any state, including those which would normally be unreachable, so it might not be a very useful trace; but we have managed to successfully get the design all the way to the solvers.

Formal setup

Depending on the state of your design you may wish to specify additional properties for the solver. In particular, we need to set up constraints for the clock and reset signals. When using Verific we can do this by binding a module which provides assumptions on the input signals like so:

[file formal.sv]
module formal_setup();
    (* gclk *) reg gclk;
    reg clk = '0;
    always @(posedge gclk)
        clk <= !clk;

    reg [3:0] rst_counter = 2;
    always @(posedge clk)
        if (rst_counter)
            rst_counter -= 1;

    wire rst = rst_counter > 0;

    always @* begin
        setup_clk: assume (veer_wrapper.clk == clk);
        setup_rst_l: assume (veer_wrapper.rst_l == !rst);
        setup_dbg_rst_l: assume (veer_wrapper.dbg_rst_l == !rst);
    end

endmodule

bind veer_wrapper formal_setup formal_setup_inst(.*);

Again we are providing a file from within the SBY file and do not need to add it to the [files] section. We do, however, need to tell Verific to read it. We do this by adding formal.sv on a new line after design/veer_wrapper.sv in the veer.f command file.

First we connect the global clock with the line (* gclk *) reg gclk;. Each rising edge of the global clock corresponds to one step (or frame) in the solver. By inverting the clk register on each posedge, each step of the solver alternates between a rising edge and a falling edge of the clk. Then we need to have an assumption which says our top level clock, veer_wrapper.clk in this case, is equivalent to clk.

We can also add a reset, using a counter to control the number of cycles it should be held high. As with the clock, we then add an assumption to the corresponding top level signal or signals. If the reset signal is active low then the assumption should be == !rst. We can add constraints (assumptions) or any other property to any signal as follows:

always @* begin
    // always high
    assume (top.a);
    // always low
    assert (!top.b);
    // deeply nested
    cover (top.x.y.z);
    // conditional
    if (rst)
        assume (top.c);
end

// SVA properties
assume property(@(posedge clk) disable iff(rst) $rose(top.d) |-> top.e == '0);

Say you wanted to see a list of properties in the design. This can be achieved with the select command in Yosys, using the -list flag and the tee option to export to a file. We might add something like the following to the [script] section:

tee -o ../props.txt log Cover cells:
tee -a ../props.txt select t:$cover -list
tee -a ../props.txt log
tee -a ../props.txt log Assert cells:
tee -a ../props.txt select t:$assert -list
tee -a ../props.txt log
tee -a ../props.txt log Assume cells:
tee -a ../props.txt select t:$assume -list

Running SBY now we get the following:

veer/props.txt

Cover cells:

Assert cells:
dma_ctrl_default/assert_dma_axi_awlen_check
** other cells of type $assert **

Assume cells:
formal_setup/setup_clk
formal_setup/setup_dbg_rst_l
formal_setup/setup_rst_l

veer/logfile.txt

SBY [veer] Writing 'veer/src/formal.sv'.
SBY [veer] Writing 'veer/src/veer.f'.
SBY [veer] Copy 'Cores-VeeR-EH1/design' to 'veer/src/design'.
SBY [veer] Copy 'Cores-VeeR-EH1/configs' to 'veer/src/configs'.
SBY [veer] Copy 'Cores-VeeR-EH1/tools' to 'veer/src/tools'.
SBY [veer] engine_0: smtbmc
...
SBY [veer] summary: engine_0 (smtbmc) returned FAIL
SBY [veer] summary: counterexample trace: veer/engine_0/trace.vcd
SBY [veer] summary:   failed assertion veer_wrapper.veer.dma_ctrl.assert_dma_axi_awlen_check at design/dma_ctrl.sv:535.32-536.81 in step 4
SBY [veer] DONE (FAIL, rc=2)

We can see from this that the dma_ctrl module is expecting a valid AXI connection, which is currently missing. We could add assumptions on the inputs that match the assertions, but we already have perfectly good properties that we can use: the assertions themselves.

Changing properties

The chformal command in Yosys enables formal properties to be changed at run time. With this command we can convert assertions to assumptions (as well as the reverse), or entirely remove properties that we are not currently interested in.

From our previous run we know that the assert cell dma_ctrl_default/assert_dma_axi_awlen_check fails. We could add the following line after calling prep to remove it:

chformal -remove dma_ctrl_default/assert_dma_axi_awlen_check

But then we would just be left with another assertion in the same module failing. This also has the side effect that if anything else in the design is relying on the (now missing) assertion being correct, it will also fail. Instead, let’s add the following:

chformal -assert -assert2assume dma_ctrl_default/assert_dma_axi_*

We can see from the command reference page for chformal (or by running calling help chformal within Yosys) that we can specify the type of formal property to target, and that the final argument is a selection rather than simply the name of a property. Thus we use a wildcard to match all of the dma_ctrl properties related to AXI, limited to just assert cells, and then convert them to assume cells. Provided the AXI is properly connected and valid, this ensures that any other properties relying on the dma_ctrl can also be verified.

The keep-going flag

At this stage of the process we may be ready to run the solver against all of our properties rather than stopping at the first failure, and increasing the depth of BMC. We can do this by adding the --keep-going flag to our engine, e.g. smtbmc --keep-going. In order to keep run time down there are a few things worth considering. First is the -flatten flag for prep. This will flatten the circuit and allow additional course grain optimizations. The next is adding cutpoints for elements which are computationally difficult to prove. This could look like the following:

[options]
mode bmc
multiclock on
depth 40

[engines]
smtbmc --keep-going

[script]
exec -expect-return 0 -- bash -c 'RV_ROOT=$PWD ./configs/veer.config'
read -f -formal veer.f
prep -flatten -top veer_wrapper
chformal -assert -assert2assume veer_wrapper/veer.dma_ctrl.assert_dma_axi_*
cutpoint t:$mul t:$mem_v2

Note that flattening the hierarchy means we have the dma_ctrl assertions need to be referenced slightly differently. Rather than dma_ctrl_default/assert... we now see veer_wrapper/veer.dma_ctrl.assert....

We have also added cutpoints for all $mul and $mem_v2 cells, i.e. multipliers and memory blocks. The cutpoint command disconnects the inputs to any matching cell, and connects the outputs to $anyseq cells, allowing the solver to to assign any value to the outputs provided it does not invalidate any assume cells. This does of course mean that any properties which rely on correct and valid multipliers or memories will now fail, but we can verify those separately.

Tasks and verification IP

This final step brings us to the veer.sby file in the source repository for this application note. Let’s start with the newly added [tasks] section and the updated [options] and [engines] sections:

[tasks]
bmc
pdr
cover
axi_bmc: axi bmc
axi_pdr: axi pdr
axi_cover: axi cover

[options]
bmc:
mode bmc
multiclock on
depth 40
--
pdr:
mode prove
multiclock on
--
cover:
mode cover
multiclock on
--

[engines]
bmc: smtbmc --keep-going
pdr: abc --keep-going pdr
cover: smtbmc

There is now a task for each of bmc, prove, and cover modes. The options for the bmc task are the same as we had before, while pdr and cover select their corresponding mode and enable multiclock. For more on how to use tasks, refer to https://yosyshq.readthedocs.io/projects/sby/en/latest/reference.html.

We also have a tag, axi, which we will be using to optionally enable verification of the dma_ctrl AXI interface we were previously converting to assumptions. The axi_bmc, axi_pdr, and axi_cover tasks then correspond the earlier tasks but with an AXI destination verification IP connected.

In the same directory as the veer.sby you have been working on, run git clone https://github.com/YosysHQ-GmbH/SVA-AXI4-FVIP to download the verification IP we will be using. Following the example in yosyshq_tabbycad_example_setup.sby, we update the [files] section and veer.f file (omitted for brevity) to load the requisite files. For the bind file, we use dma_destination.sv, a modified version of destination template configured to match the interface in dma_ctrl.

[files]
Cores-VeeR-EH1/design
Cores-VeeR-EH1/configs
Cores-VeeR-EH1/tools

axi:
# Packages
SVA-AXI4-FVIP/AXI4/src/amba_axi4_protocol_checker_pkg.sv
SVA-AXI4-FVIP/AXI4/src/amba_axi4_low_power_channel.sv
SVA-AXI4-FVIP/AXI4/src/axi4_spec/amba_axi4_single_interface_requirements.sv
SVA-AXI4-FVIP/AXI4/src/axi4_spec/amba_axi4_definition_of_axi4_lite.sv
SVA-AXI4-FVIP/AXI4/src/axi4_spec/amba_axi4_atomic_accesses.sv
SVA-AXI4-FVIP/AXI4/src/axi4_spec/amba_axi4_transaction_structure.sv
SVA-AXI4-FVIP/AXI4/src/axi4_spec/amba_axi4_transaction_attributes.sv
SVA-AXI4-FVIP/AXI4/src/axi4_spec/amba_axi4_low_power_interface.sv
SVA-AXI4-FVIP/AXI4/src/axi4_lib/amba_axi4_write_response_dependencies.sv
SVA-AXI4-FVIP/AXI4/src/axi4_lib/amba_axi4_exclusive_access_source_perspective.sv

# Modules containing the properties
SVA-AXI4-FVIP/AXI4/src/amba_axi4_protocol_checker.sv
SVA-AXI4-FVIP/AXI4/src/amba_axi4_read_address_channel.sv
SVA-AXI4-FVIP/AXI4/src/amba_axi4_read_data_channel.sv
SVA-AXI4-FVIP/AXI4/src/amba_axi4_write_data_channel.sv
SVA-AXI4-FVIP/AXI4/src/amba_axi4_write_response_channel.sv
SVA-AXI4-FVIP/AXI4/src/amba_axi4_write_address_channel.sv

# Bind file
dma_destination.sv
--

Where before we were unconditionally converting the dma_ctrl AXI assertions, we now only want to do so if we are not running one of the axi_ tasks. The rest of our script section remains the same:

[script]
exec -expect-return 0 -- bash -c 'RV_ROOT=$PWD ./configs/veer.config'
read -f -formal veer.f
prep -flatten -top veer_wrapper

# dma_axi requires axi to be setup
# otherwise, convert axi asserts to assume
~axi: chformal -assert -assert2assume veer_wrapper/veer.dma_ctrl.assert_dma_axi_*

cutpoint t:$mul t:$mem_v2

The dma_ctrl module itself needs a minor adjustment which is included in dma_ctrl.patch. This change removes the clock gating while still keeping the dma_bus_clk signal connected. And finally, we need to add a constraint to the formal.sv file to keep the veer_wrapper.dma_bus_clk_en high.

With this, we can now perform verification on the VeeR core via bounded and unbounded model checking as well as generate traces for all cover statements, and we can optionally enable verification of the DMA AXI controller.