CVXIF Assertions Updates

[silabs-robin]

Hi. About XIF assertions. Here are 3 recommendations for what it should include (ref. our previous meeting).

Use "assert-assume" macro to have asserts toggle-able to work as assumes. Three parameters must be supported for the assertion module: 1) cpu-perspective, 2) coproc-perspective, 3) always assert. Example, x_issue_req_t has signals that must be "stable" under certain conditions, while this must be asserted on the cpu's outputs, a coprocessor might assume that its inputs are driven according to spec. (I have started on this, so I can PR the macro itself in a while.)

Split the assertion file to isolate "protocol-specific" asserts. Suggested split: 1) protocol-specific, 2) integration-specific (if necessary), and 3) core-specific, and maybe 4) ISA-extension-specific. (The important point is that protocol-specific is separated, the three other categories are just suggestions so feel free to judge what is the best fit.) Def: Protocol-specific, XIF-related info deducable merely from the interface signals. Def: Integration-specific, XIF-related info requiring probing into other modules in addition to the interface signals.

Asserts should capture all the assertion check items from the vplan. (IMO, as many vplan items as possible should include assertion checks.) One could also add cover properties to check for certain scenarios, and covergroups to check i.a. the input signals and/or crosses of them.

Hi @zelkacimi. Since you are the author of the assertions file I wanted to tag you on this issue.

[silabs-robin]

Relates to https://github.com/openhwgroup/core-v-verif/issues/1195 and https://github.com/openhwgroup/core-v-verif/issues/1192

[ZElkacimi]

hello @silabs-robin I got your idea, the first version of the agent did not include many assertions but coming versions will. Moreover, I would be interested on your PR about "assert-assume" macro, since for now I use only "assert", please tag me on it. Thanks

[silabs-robin]

Hi @ZElkacimi. I have made an example "testbench" for using this assert-assume macro.

(First, I tried to "git cherry-pick" to get access to the cvxif assertions, but that got messy so I just made a "toy" example that I can post here on this issue.)

The following example has been tested in formal. If you have access to a formal tool to test this in, then that works better than simulation. You can try tweaking the parameters of the assertion module below to see how the formal tool reacts differently.

---

Here is the macro itself:

package cv_assert_pkg;

`define CV_ASSERT 1
`define CV_ASSUME 0

`define CV_GEN_PROP(name, assert_param, prop)                    \
  generate                                                       \
    if (``assert_param`` == `CV_ASSUME) begin : gen_asm_``name`` \
      ``name`` : assume property (``prop``);                     \
    end else begin : gen_asrt_``name``                           \
      ``name`` : assert property (``prop``);                     \
    end                                                          \
  endgenerate


// This uvm define is only temporarily here for compilation to work
`define  uvm_error(ID, MSG)  ;

endpackage : cv_assert_pkg

Now, a DUT to work with:

module dut (
  input logic clk_i,
  input logic rst_ni,

  input logic       en_i,
  input logic [7:0] dat_i,

  output logic       en_o,
  output logic [7:0] dat_o
);

  always @(posedge clk_i, negedge rst_ni) begin
    if (!rst_ni) begin
      en_o  <= '0;
      dat_o <= '0;
    end else begin
      en_o  <= en_i;
      dat_o <= dat_i;
    end
  end

endmodule : dut

Assertions using the CV_GEN_PROP macro:

module asserts
  import cv_assert_pkg::*;
#(
  parameter IS_MONITOR = 1,
  parameter IS_MASTER  = 0,
  parameter IS_SLAVE   = 0
) (
  input wire clk_i,
  input wire rst_ni,

  input wire       en_i,
  input wire [7:0] dat_i,

  input wire       en_o,
  input wire [7:0] dat_o
);

  localparam MASTER_ASSERT = IS_MONITOR ? `CV_ASSERT : (IS_MASTER ? `CV_ASSERT : `CV_ASSUME);
  localparam MASTER_ASSUME = IS_MONITOR ? `CV_ASSERT : (IS_MASTER ? `CV_ASSUME : `CV_ASSERT);

  default clocking @(posedge clk_i); endclocking
  default disable iff !(rst_ni);

  a_legal_assert_mode: assert property (
    $onehot({IS_MONITOR, IS_MASTER, IS_SLAVE})
  ) else `uvm_error("someinfotag", "assertion module wrongly parameterized");

  property p_stable_while_enabled(en, dat);
    en [*2]
    |->
    $stable(dat);
  endproperty : p_stable_while_enabled
  `CV_GEN_PROP(a_stable_out, MASTER_ASSERT, p_stable_while_enabled(en_o, dat_o));
  `CV_GEN_PROP(a_stable_in,  MASTER_ASSUME, p_stable_while_enabled(en_i, dat_i));

endmodule : asserts

And a bind file to connect it:

module binder;

  bind dut
    asserts #(
      .IS_MONITOR (0),    // Try changing these params
      .IS_MASTER  (1)
    ) my_asserts_i (
      .*
    );

endmodule : binder

[silabs-robin]

The macro should preferably be somewhere in the core-v-verif/lib/ directory.

We should also try to merge the cva6 dev branch with master soon! It would benefit us all if we can start working on the same XIF files. Getting access to these assertions would be very nice, but cherry-picking didn't work so well, so plain merging and syncing with master should do the trick. (We can talk with Mike about this in some other thread.)

If you disagree with the naming of the macro or find a bug in this example or anything then please just call it out and we can discuss (I am not even sure myself if I like the name "CV_GEN_PROP").

[MikeOpenHWGroup]

We should also try to merge the cva6 dev branch with master soon!

Yes, I completely agree. @JeanRochCoulon

[ZElkacimi]

Hello all,

Note: a new PR for the agent is available here: [https://github.com/openhwgroup/core-v-verif/pull/1229]

I tried your macro but currently I don't have access to a formal tool so I couldn't see how it really works. However, it's nice to have it somewhere in lib, I will update the assertion module whenever the macro is available in lib/ For the name of the macro, I suggest CV_ASSERT_ASSUME_GEN but I'm not also sure if this name is suitable or not. I have added many assertions and cover properties to the assertion module but without the separation you have suggested, for me, they are all always assert but can be updated later following your comments.

Looking forward for your feedback

Thanks

[silabs-robin]

Closed as stale. (Might resume if it becomes relevant again.)