Use cv32e40p_wrapper to bind in RTL assertions.

[MikeOpenHWGroup]

Hi @Silabs-ArjanB and @davideschiavone, this is a demonstration of how we can use the new cv32e40p_wrapper to bind in "designer assertions" into the RTL. This was discussed in the OpenHW: Extracting assertions from the RTL email thread.

This demo moves the assertions in cv32e40p_prefetch_controller module up to the wrapper. Once we settle on an implementation it will be straightforward to move the remaining assertions.

There are some minimal updates required to the verification environment to support this. If you clone the regression_test branch of https://github.com/MikeOpenHWGroup/core-v-verif, you can run "make sanity" and see it in action.

[Silabs-ArjanB]

Hi Mike,

Thanks for showing an example. I agree with the general approach, but I have some comments on specifics. For us (meaning people working in the cv32e40p repos) it is a must that the design assertions can be used as before in a non-UVM environment as well. I agree that we want to use error reporting from uvm_pkg::*, but maybe this needs to be go through some indirection (I will check with Steve what he recommends for this). Also I think we need two manners to disable assertions (one via a global ifdef, one per file). The global mechanism you removed; I am fine with the ifdef per assertion file, but then it needs to go arround the 'bind'. for the local mechanism I will again ask Steve to propose something.

[Silabs-ArjanB]

Also probably we want the assertions in a separate (new) directory.

[MikeOpenHWGroup]

Thanks for the quick review @Silabs-ArjanB. To your points:

it is a must that the design assertions can be used as before in a non-UVM environment

You can still use the UVM messaging service (e.g. uvm_error()), without having a dependency on a full UVM environment. All you need to do is to import the package (already done) and add a compile switch in the Makefile. Alternatives are very ugly.

Also I think we need two manners to disable assertions

I would recommend we reinstate the global control via a compile-time macro. Individual file control is messy and best left to the simulator to deal with, so I would recommend we only support global control in the code. I'll add that back in to this PR.

we want the assertions in a separate (new) directory.

That is my instinct as well.

I will update this PR to reinstate the global control of the macros and also put the assertions in their own directory.

[MikeOpenHWGroup]

I will update this PR to reinstate the global control of the macros and also put the assertions in their own directory.

Done.

[Silabs-ArjanB]

Please put the ifdefs as high level as possible, e.g. around the bind, not in the assertion files

[MikeOpenHWGroup]

Please put the ifdefs as high level as possible, e.g. around the bind, not in the assertion files

That was the first thing I tried. Alas, Verilator needs both. Another way to do this would be with manifest file control. Its my understanding you are investigating something like this so maybe we can kill two birds with that one stone.

[Silabs-ArjanB]

Please put the ifdefs as high level as possible, e.g. around the bind, not in the assertion files

That was the first thing I tried. Alas, Verilator needs both. Another way to do this would be with manifest file control. Its my understanding you are investigating something like this so maybe we can kill two birds with that one stone.

I am not investigating anything related to this. Maybe you are talking about the FuseSoc support; yes, that might solve it, but I am not working on it.

[MikeOpenHWGroup]

[@Silabs-ArjanB ] Please put the ifdefs as high level as possible, e.g. around the bind, not in the assertion files

[@MikeOpenHWGroup] That was the first thing I tried. Alas, Verilator needs both. Another way to do this would be with manifest file control. Its my understanding you are investigating something like this so maybe we can kill two birds with that one stone.

[@Silabs-ArjanB ] I am not investigating anything related to this. Maybe you are talking about the FuseSoc support; yes, that might solve it, but I am not working on it.

I see. This creates a challenge for Verilator because it cannot compile Assertions (or the Tracer) and the way the manifest is currently set up, the tool must compile them all, even if they are not to be included. I've pushed in a alternative method which will work, but it means I needed to edit the manifest and include the Tracer, Assertions, etc from the wrapper itself. This puts all the compiler macros in one file (the Wrapper), but the need to be in two places.

[Silabs-ArjanB]

Why are these 3 files commented out; you will need them in core-v-verif

[MikeOpenHWGroup]

This was done while trying to "put the binds as high as possible" so that there would only be one set of compiler macros to control compilation and binding of the tracer and assertions. Verilator cannot handle the tracer, assertions, etc, so if these modules cannot have conditional compile macros, then they cannot be in the manifest.

The proposed solution is to place conditionally compiled tick-includes in the wrapper.

[Silabs-ArjanB]

My point is that you still need these files to be loaded/compiled in core-v-verif, so if you do not put them in the manifest your code in core-v-verif won't compile.

[MikeOpenHWGroup]

That is correct for the UVM environment. The Makefles know this and set the appropriate macros that compile in the tracer. Take a look at the top of cv32e40p_wrapper.sv to see what I mean. Verilator cannot parse the tracer, so the Makefiles for the core testbench do not use these macros.

[Silabs-ArjanB]

I don't get it, but that's fine. I think you will simply be missing files in core-v-verif if you try to compile for UVM. (Anyway, you can leave them commented out).

[MikeOpenHWGroup]

The inclusions are at the top of cv32e40p_wrapper.sv not in the manifest:

`ifdef CV32E40P_SVASSERTIONS
  `include "cv32e40p_prefetch_controller_sva.sv"
`endif

`include "cv32e40p_core_log.sv"

`ifdef CV32E40P_APU_TRACE
  `include "cv32e40p_apu_tracer.sv"
`endif

`ifdef CV32E40P_TRACE_EXECUTION
  `include "cv32e40p_tracer.sv"
`endif

[Silabs-ArjanB]

Okay, now I get it. That is quite 'non-conventional'

[MikeOpenHWGroup]

I don't like it much myself. Once we get a proper manifest generator tool in place we can get rid of this. The single benefit is that the compiler macros (the tick-ifdefs) are all in one file.

[Silabs-ArjanB]

Hi @MikeOpenHWGroup The Cadnce JasperGold formal tool will neither accept the uvm package import nor the use of `uvm_error, so the proposed syntax will simply not work for us. The main goal of these design assertions is usage during Formal verification. If you propose some ifdef based approach, then that will probably be acceptable (but ugly).

[MikeOpenHWGroup]

Cadence JasperGold formal tool will neither accept the uvm package import nor the use of `uvm_error,

Interesting. In one of my past lives we did get JG to compile the uvm package and its associated macros. Basically, the tool just ignored them. Let me reach out to some ex-colleagues to see how we did this.

If you propose some ifdef based approach, then that will probably be acceptable (but ugly).

What I would probably propose would be the use of a macro that would use uvm_error for simulation and exclude it for synthesis and formal. Before we go there, let's see what I can dig up.

[MikeOpenHWGroup]

Hi @Silabs-ArjanB, I finally have a reply to a question you raised earlier:

The Cadnce JasperGold formal tool will neither accept the uvm package import nor the use of `uvm_error, so the proposed syntax will simply not work for us.

An ex-colleague of mine, who is a full-time formal verification engineer and very experienced in JG, tells me that the action block of SVA asserts is ignored by formal tools, so we can put whatever we need in there for simulation. In our case, that is everything in the else clause of the assertion statement:

property p_no_transaction_count_overflow_1;
     @(posedge clk) disable iff (!rst_n) (cnt_q == DEPTH) |-> (!count_up || count_down);
endproperty

a_no_transaction_count_overflow_1:
    assert property(p_no_transaction_count_overflow_1)
    else
        `uvm_error("Prefetch Controller SVA",
                 $sformatf("Overflow condition detected: cnt_q==DEPTH==%0d, count_up==%0d, count_down==%0d",
                           cnt_q, DEPTH, count_up, count_down))

We may need to have conditional compiler macros (tick ifdefs) around the import statement.

[Silabs-ArjanB]

Hi @MikeOpenHWGroup I tried with an ifedf around the import statement, but JG is not ignoring the else clause, but it is giving a "ERROR (VERI-1158)" instead about the "use of undefined macro 'uvm_error''". Anyway, you can still go ahead with using the following ifndef:

ifndef FORMAL import uvm_pkg::*; endif

and then we will define our own dummy uvm_error implementation to get around the error when using Jasper Gold (and use the real uvm_error otherwise when not using Jasper Gold).

[MikeOpenHWGroup]

Hi @Silabs-ArjanB and @davideschiavone. This PR has been hanging out for more than a month. As I understand things, it was blocked by PR #436. That one is merged in now (plus several others), so can we get to this one?

BTW, both of you are Committers, so either can merge it.

[Silabs-ArjanB]

Please use `ifdef CV32E40P_ASSERT_ON instead. That is what we assume in our Makfiles, etc.

[Silabs-ArjanB]

Please use `ifdef CV32E40P_ASSERT_ON instead. That is what we assume in our Makfiles, etc.

[Silabs-ArjanB]

This file is now fully out of date with https://github.com/openhwgroup/cv32e40p/blob/master/rtl/cv32e40p_prefetch_controller.sv. Please re-add the current set of assertions from https://github.com/openhwgroup/cv32e40p/blob/master/rtl/cv32e40p_prefetch_controller.sv

[Silabs-ArjanB]

Please make sure that the assertions are included in the Makefile from example_tb/core as well and that 'hello world' runs there including the asserstions

[MikeOpenHWGroup]

Sorry, here I will have to say "no". I am not the owner/maintainer of example_tb and in fact have asked several times for it to be removed.

[MikeOpenHWGroup]

Hi @Silabs-ArjanB, @davideschiavone. I have made this pull-request up-to-date with the head of the master branch of the RTL and made edits as per @Silabs-ArjanB, recommendations. I have also wrapped the SV property in the cv32e40p_aligner with compiler directives to exclude it for Verilator compiles.

Please try to get this merged in quickly as a significant amount of additional work cannot make progress until this is "in". Thanks.

[Silabs-ArjanB]

@MikeOpenHWGroup Most feedback given has not been taken into account; I will merge this anyway and then do another commit to make the required fixes (worst one was that assertions were removed all together)