(Asserts) Tool Compatibility Issues

stefanlippuner commented 4 years ago

Hi all!

As you may know, we are currently using your USB FS device implementation, to which I've also contributed some of our changes. @vogelpi and I have also been looking for a good way for us to track your (upstream) repository. Unfortunately some of your recent changes (mostly to the assertion primitives) have caused a lot of issues for me, because the used constructs are not supported by our tools. I can fix this with patches/differences to your code, but this makes merging any changes extra difficult. I wanted to start a discussion on whether you'd be willing to tune your code in order to improve compatibility with a larger set of tools.

On our side, we currently need to support: Incisive 15, RTL Compiler 14 (old), Genus 15 (old), QuestaSim 10.7 and Design Compiler.

Observed Issues

Default Arguments for Defines

// From prim_assert.sv

// Assert a concurrent property directly.
// It can be called as a module (or interface) body item.
`define ASSERT(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \
`ifdef INC_ASSERT                                                                        \
  __name: assert property (@(posedge __clk) disable iff (__rst !== '0) (__prop))         \
    else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop))                   \
`endif
// Note: Above we use (__rst !== '0) in the disable iff statements instead of
// (__rst == '1).  This properly disables the assertion in cases when reset is X at
// the beginning of a simulation. For that case, (reset == '1) does not disable the
// assertion.

This is currently my main issue. Genus 15 does not support default parameters for defines, which means I can only have a single version of each macro. The only thing I could come up with is disabling all the assertions (during synthesis) and thus maintaining a separate version of all the primitives.

Multi-line Assertions

// From: tlul_assert.sv

  `ASSERT_VALID_DATA(aKnown_A, h2d.a_valid, {h2d.a_size, h2d.a_source, h2d.a_address,
      h2d.a_mask, h2d.a_user}, clk_i, !rst_ni)

This kind of expression caused issues with the elaboration in QuestaSim 10.7, which considered it unterminated. To work around it, we had to disable these assertions. I've also seen similar issues with Genus, but I was to remove the primitives, since they're not used in the USB peripheral.

Localparams

// From: usb_fs_nb_pe.sv
module ... #( // ...
  localparam int unsigned PktW = $clog2(MaxPktSizeByte) // derived parameter
);

Localparams within the port declaration are not supported by Incisive 15. So far I've manually replaced them with params in our repository.

Possible Solutions

As I can't do anything about these tools, I have to find a way to get this to work on our side and then keep it working with your frequent updates. I can maintain patches to apply to your codebase to make it work in our setup, probably disabling all the assertions. This essentially turns every update from your repository into a lot of work. Perhaps this could be partially automated, but I still don't think this is sustainable from my side. It would also not help any other people with similar tools and issues.

Alternatively, it might be nicer to implement some workarounds on your side. One idea would be disabling the assertions outside the macros, i.e. using

`ifdef INC_ASSERT
  // Flush and Write Enable cannot be asserted same time
  `ASSUME(ExFlushValid_M, flush_i |-> !valid_i, clk_i, !rst_ni)

  // While in flush state, new request shouldn't come
  `ASSUME(ValidIDeassertedOnFlush_M,
          flush_st == FlushWait |-> $stable(valid_i),
          clk_i, !rst_ni)

  // ...
`endif

instead of having the same switch inside the assert macros. This way parsing the assert macro can be completely avoided for the tools that have problems with it. Assertions would still not work with those tools, but at least they could run the code with a limited set of changes.

What do you think? Would you be willing to make some changes to your assertions to ease support for older/worse tools? Or do you have better ideas?

imphil commented 4 years ago

Thanks for opening this issue. While we try to support recent versions of the most frequently used tools, supporting older versions is effectively a race to the bottom. That being said, we're willing to compromise as long as it doesn't affect productivity or correctness too much.

On localparam: we went in circles with that one already a couple times. (lowRISC/opentitan#50, https://github.com/lowRISC/style-guides/pull/15). All current tools we've tested support it. Can you check if the current version of Genus supports it?
On the assert macros: I'm not sure we can find a good solution for that, other than removing the defaults again. Also on this one: does the current version of Genus supports it?

So overall:

If there's something that doesn't work in the most recent version of Genus, we have a strong incentive to find a workaround. So please double-check that if possible.
If not, I propose you give tools like sv2v a try, which should also help you with more incompatibilities you might run into in the future.

stefanlippuner commented 4 years ago

On localparam: That was actually a mistake on my side, Genus 15 does support it, but the Incisive simulator does not support it. It sounds like it's supported in newer (Xcelium) versions. On the macros: The newest version of Genus seems to support it, even though the documentation states otherwise.

Unfortunately it is not really possible for us to upgrade to the newer tool versions due to licensing issues (it's just too expensive).

I understand that you have to draw the line somewhere and don't necessarily want to support old tools. The mish mash of SystemVerilog support in tools is really annoying. I'll think about using sv2v.

towoe commented 4 years ago

@stefanlippuner you can have a look at Ibex here and here for some experimental examples of sv2v usage.

sjgitty commented 4 years ago

@stefanlippuner thanks for raising this, and as @imphil mentioned it is an unfortunate race to the bottom that we want to avoid. One split-the-baby proposal we could consider is for the ASSERT macros in this area (I only count 12 in the USB code base) we define assertion macros just for USB that are "dumbed down" (keeping the definition of these isolated into the USB code space). This could work for those 12, but still doesn't solve the tlul_assert inclusion files. We really would prefer us not revert the whole database back to pre-default-era assertions. Let us know your thoughts on sv2v

stefanlippuner commented 4 years ago

Thanks for your responses! I've played around with sv2v a bit. It seems to have similar issues with assertions. First I had to disable your assertions (with defining SYNTHESIS) and then I had to remove some of my local assertions too. After this the tool generated an output, but this was unfortunately not valid Verilog. I would also prefer to not add such an experimental tool to our workflow. I would actually prefer having a script that removes the assertions over using sv2v.

I understand that you don't want to change things in your codebase to account for older tools. I will therefore close this issue. On our side I will not track the changes to your primitives for now. If this becomes a problem I will probably use a script to remove the assertions.

lowRISC / opentitan