Working with a CV32 core¶

This example uses the CV32E40X Design-Verification environment: converting the existing Jasper script to an equivalent SBY implementation. Unlike the previous example, let’s skip straight to using the code in this repository.

In the cv32e40x directory, run make clone. This will clone the CORE-V verification project, the CV32E40X Design-Verification environment, and the CV32E40X RISC-V core.

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.

The existing Jasper script¶

cv32e40x/core-v-verif/cv32e40x/fv/jaspergold.tcl¶

proc cvfv_rerun {} {
    clear  -all

    # Message Severities
    ## Error on file not found
    set_message -error WNL074
    ## Allow omitted param defaults
    set_message -info VERI-1818
    ## Allow parameter treated as localparam
    set_message -info VERI-2418
    ## Allow empty port in module declaration
    set_message -info VERI-8026
    ## Allow multiplier blackboxing
    set_message -info WNL018

    # Analyze & Elaborate
    analyze  -sv12  -f fv.flist
    elaborate  -top uvmt_cv32e40x_tb  -extract_covergroup

    # Clock & Reset
    clock  clknrst_if.clk
    reset  ~clknrst_if.reset_n

    # Assumes
    assume  -from_assert  {*_memory_assert_i.u_assert.a_r_after_a}
    assume  -from_assert  {*.obi_*_memory_assert_i.*.a_*par}
    assume  -from_assert  {*integration_assert_i.a_stable_*}
    assume  -from_assert  {*integration_assert_i.a_aligned_*}
    assume  -from_assert  {*integration_assert_i.a_no_scan_cg}
}

cvfv_rerun

Converting to SBY¶

In order to run the cv32 design verification with SBY and Verific we need to make a few adjustments. First we will look at the Yosys script equivalent, then the additional clock/reset setup, and finally the changes needed to the source code.

The Yosys script¶

cv32e40x.sby [script] section¶

# Message Severities
## Allow omitted param defaults
verific -set-info VERI-1818
## Allow parameter treated as localparam
verific -set-info VERI-2418
## Allow empty port in module declaration
verific -set-info VERI-8026

# Additional warning/error messages
## Ignore covergroup warnings
verific -set-info VERI-1333
## Ignore 'new' operator errors
verific -set-info VERI-1685
## Ignore missing driver warnings (reported in Yosys)
verific -set-info VDB-1002

# Analyze & Elaborate
verific -f -sv2012 -formal cv32e40x.f
## formal clock and reset setup
verific -formal formal_setup.sv
## import from verific to yosys
hierarchy -top uvmt_cv32e40x_tb
## cut mult
### should match cv32e40x_ex_stage(B_EXT=B_NONE_cv32e40x_pkg,M_EXT=M_cv32e40x_pkg)_0/mul.mult_i
cutpoint t:$mul
## this flatten is needed to work around an issue with SV interfaces
flatten
## prepare design
prep -flatten

# Assumes
chformal -assert2assume */*_memory_assert_i.u_assert.a_r_after_a
chformal -assert2assume */*.obi_*_memory_assert_i.*.a_*par
chformal -assert2assume */*integration_assert_i.a_stable_*
chformal -assert2assume */*integration_assert_i.a_aligned_*
chformal -assert2assume */*integration_assert_i.a_no_scan_cg

Comparing this side by side with the Jasper script we see that the “Assumes” block at the end is almost identical, switching out assume -from_assert for the Yosys command chformal -assert2assume. We also see that the “Message Severities” block has re-used the same three VERI-#### severity downgrades. The “Error on file not found” is the default behaviour for Yosys/Verific so is unnecessary, and the “multiplier blackboxing” we handle explicitly later. The first two extra downgrades are used to ignore some warnings/errors which Verific raises when encountering unsupported UVM constructs, while the last is added to avoid duplicating warnings that Yosys will also report later in the flow.

This just leaves us with the “Analyze & Elaborate” and “Clock & Reset” blocks. Our first line looks very similar; using the sv2012 standard and loading the source code filelist. Formal clock and reset setup in Yosys is more explicit than in Jasper and is covered in the next section. In Yosys we use the cutpoint command to perform multiplier blackboxing. We specify that all cells of type $mul, i.e. any multipliers, should be replaced with a cutpoint; disconnecting the cell inputs and replacing the output drivers with $anyseq cells which the solver can assign any value to at each step. Finally we call prep to prepare the design for verification.

Setup clock and reset¶

In Yosys we declare our top level clock and counter in SystemVerilog, binding the formal_setup module to our top level module to provide assumptions on those signals.

cv32e40x.sby [file formal_setup.sv] section¶

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 (uvmt_cv32e40x_tb.clknrst_if.clk == clk);
        setup_rst: assume (uvmt_cv32e40x_tb.clknrst_if.reset_n == !rst);
    end

endmodule
bind uvmt_cv32e40x_tb formal_setup formal_setup_inst(.*);

In the Yosys script then we see the following line which loads this module, and the subsequent call to hierarchy ensures that the uvmt_cv32e40x_tb module is selected as the top level and the formal_setup module is included within it.

verific -formal formal_setup.sv

Patching the source¶

The Verific front-end for Yosys does not support UVM, and running SBY at this point will result in errors. While there are some error messages that we can simply downgrade and have Verific ignore them while continuing to parse the design, there are others which are not recoverable and we need to comment out the relevant source code.

Included in the source repository for this documentation are two patches for the cv32 verification setup. The core.patch disables code in the core itself, while dv.patch disables code in the testbench. The offending code is typically a formal property which performs an assignment when triggered, a feature not supported in Verific. We also adjust the clock gate to a form that is supported.

Running SBY¶

Finally we are able to run the design in SBY and get traces for cover statements and failing properties. Because of the complex nested filelist structure of the cv32 core and verification environment, we have opted for a similar reliance on variables exported by makefile. To run SBY, call make sby-[task] in the cv32e40x directory where [task] is one of bmc | pdr | cover as in the previous VeeR core example.

Note

Due to the size of the cv32 core and the number of properties, the solvers used by SBY can take a very long time to finish. Indeed they may not finish running at all without requiring a timeout, and improvements for handling large designs are being worked on.