Enable SVA in Verilator

[michael-platzer]

This PR removes the ifndef .. endif blocks that exclude the assertions from Verilator simulation, thus enabling them in Verilator as well. Hence, the PR fixes #199. As explained in that issue, Verilator has had support for assert properties since at least version 3.922 released in 2018 and support for the implication operator has been added in version 4.026 released in 2020.

Three files use a default disable (e.g., default disable iff !rst_ni;), which is not supported by Verilator. The default disable has been left in place, but additionally a disable statement has been added to all assert properties of those files.

Note that stream_xbar and stream_omega_net both have the following default disable, which appears to be incorrect:

https://github.com/pulp-platform/common_cells/blob/2bd027cb87eaa9bf7d17196ec5f69864b35b630f/src/stream_xbar.sv#L169

Given the suffix of rst_ni, the reset signal appears to be inverted (i.e., low active) and the SVA should probably be disabled if rst_ni is low rather than high. I have not modified the default disable for these files but the individual disable statements for each assert property disable the assertion if rst_ni is low instead. Please let me know whether this default is intended behavior or whether this should be fixed.

All modified files lint successfully in Verilator 5.002.

[michael-platzer]

Ping @niwis :alarm_clock: :upside_down_face:

[niwis]

Thanks a lot, @michael-platzer! I had a chat with @bluewww, and perhaps it would make sense to keep the ability to turn off assertions without doing so (at least per default) for verilator. This would imply replacing `ifndef VERILATOR by something more generic like `ifndef ASSERTS_OFF. Then the user could decide individually whether to include the assertions for a project/target. What do you think?

I agree that the default disable iff in stream_xbar and stream_omega_net looks wrong and should probably be fixed.

[michael-platzer]

Thanks @niwis for the feedback, I have replaced the `ifndef VERILATOR by `ifndef ASSERTS_OFF as you suggested. The last two commits fix the default disable in stream_xbar and stream_omega_net.

Please let me know if you are happy with the changes.

[bluewww]

I think its better if we name the macro COMMON_CELLS_ASSERTS_OFF. This allows people to be more selective about the assertions. @niwis

[niwis]

@michael-platzer sorry for the back and forth, but could you rename the macro accordingly? Then we can merge this

[michael-platzer]

@michael-platzer sorry for the back and forth

No worries :slightly_smiling_face: Macro is renamed.

[niwis]

Thanks a lot! Could you fix the exceeding line lengths for linting to pass?

[michael-platzer]

Could you fix the exceeding line lengths for linting to pass?

Done, CI looks good now.