Replace all asserts & assumes with macros from `assertions.svh` #233

michael-platzer · 2024-09-18T13:38:06Z

This PR replaces all assertions (and assumes) in the common cells sources with macros from assertions.svh.

Additionally, the assertions.svh itself is modified as follows:

Some defines (such as the guard block at the start of the header) are renamed for consistency and to avoid name collisions in the same style as in registers.svh.
The `ifndef VERILATOR is removed because Verilator has supported assertions for a while now.
An option to override any of the default defines that cause assertions to be turned off (such as SYNTHESIS) is added (so even if a tool defines, e.g., SYNTHESIS, it still has the option to forcefully enable assertions by also defining ASSERTS_OVERRIDE_ON now — yes, there are tools out there that require that 🙄).
Helper macros are undefined at the end of the file (a comment did claim that this was already the case, but it was not).
An optional extra argument is added to all assertions macros, which allows to specify a custom error message to be displayed when the assertion fails. For backwards compatibility, this extra argument is added at the end and defaults to "".

In order to replace all the assertions in the sources while avoiding typos and other oversights as best as possible, I have replaced almost all of them using sed commands. The specific commands used for each change are part of the respective commit messages.

Some noteworthy subtle changes that go along with this move:

The macros in assertions.svh require that all assertions have a name, so I added one for all those who did not have one (and I tried to hard to keep them consistent).
So far, assertions used a mix of $fatal, $error, and sometimes $warning to report failing assertions. The macros in assertions.svh universally use $error and all instances of $fatal are now changed to $error. I reviewed all those that used $warning but since they all appear to be pretty critical issues as well, they now also use the macros which report an $error (the affected files are src/addr_decode_dync.sv, src/cdc_fifo_gray_clearable.sv, src/multiaddr_decode.sv, and src/spill_register_flushable.sv, so the authors of these @WRoenninger, @fabianschuiki, @zarubaf, @meggiman, and @colluca might want to take a look).
Assertions that were previously declared as assert initial or assert final are now immediate assertions in a initial or final block, respectively.
src/rr_arb_tree.sv, src/stream_omega_net.sv, and src/stream_xbar.sv previously used a default disable (e.g., default disable iff (~rst_ni);), which btw is also not supported by Verilator. Each assertion macro has an disable iff !rst_ni instead, so I removed those.

Also, the following files make use of assertions in a pretty advanced/adventurous way (which btw also causes Verilator 5.018 to fail as reported in #229):

src/addr_decode_dync.sv: Includes a huge always block with assumes all over the place.
src/multiaddr_decode.sv: Again an always block with an assume in it.

I'd like to ask the respective authors (@WRoenninger and @colluca) to review the changes to these files (you are of course welcome to review changes to the other files as well).

Merging this PR closes #232.

…TS_OFF

colluca · 2024-09-18T13:43:13Z

@michael-platzer thanks for the PR :)

I will not be able to review this before Monday, but I will definitely have a look then.

michael-platzer · 2024-09-24T06:25:11Z

I reckon that this is a pretty large PR. @niwis Would you rather have me split this into multiple smaller PRs? Perhaps starting with the changes to assertions.svh only?

colluca

Thanks for the PR @michael-platzer!

It looks good to me for the most part.

One thing I would perhaps change, is to move all include statements at the beginning of the files, rather than within the modules. I believe this is more consistent with other include statements and better aligned with one's expectation on where to find included files. Also, for files defining multiple modules e.g. cdc_2phase_clearable this would mean we only need to include it once.

Could we also move COMMON_CELLS_ASSERTS_OFF to assertions.svh for consistency? As of now, some but not all assertions would be disabled, which I think would go against expectation.

Finally, in the PR description (and later in the changelog) I would mention that some assertions which did not define a disable iff condition now do after aligning them to use the ASSERT macro, and I would list the files affected by this change (e.g. stream_to_mem.sv).

include/common_cells/assertions.svh

src/stream_omega_net.sv

src/addr_decode_dync.sv

src/onehot_to_bin.sv

src/rr_arb_tree.sv

src/mem_to_banks_detailed.sv

Partially reproducible with the following sed command: sed -zi 's/\nmodule/\n`include "common_cells\/assertions.svh"\n\nmodule/g' `grep assert src/*.sv` Requires extensive cleanup.

Mainly reproducible with the following sed command: sed -zi 's/$[a-zA-Z_][a-zA-Z0-9_]*$[ \t\r\n]*:[ \t\r\n]*assert *property[ \t\r\n]*([ \t\r\n]*@(posedge *$[a-zA-Z_][a-zA-Z0-9_]*$)[ \t\r\n]*disable *iff *([~!]$[^)]*$)[ \t\r\n]*$[^;]*$[ \t\r\n]*)[ \t\r\n]*else[ \t\r\n]*\$fatal[ \t\r\n]*(1,[ \t\r\n]*$[^;]*$[ \t\r\n]*);/`ASSERT(\1, \4, \2, !\3, \5)/g' src/*.sv Some manual cleanup required for one assertions without message, as well as removal of redundant parenthesis via: sed -i 's/`ASSERT($[^,]*$, ($[^,]*$),/`ASSERT(\1, \2,/g' src/*.sv

Mainly reproducible with the following sed command (as well as a similar variant that matches assertions with $error instead of $fatal): sed -zi 's/assert *property[ \t\r\n]*([ \t\r\n]*@(posedge *$[a-zA-Z_][a-zA-Z0-9_]*$)[ \t\r\n]*disable *iff *([~!]$[^)]*$)[ \t\r\n]*$[^;]*$[ \t\r\n]*)[ \t\r\n]*else[ \t\r\n]*\$fatal[ \t\r\n]*(1,[ \t\r\n]*$[^;]*$[ \t\r\n]*);/`ASSERT(NAME_ME, \3, \1, !\2, \4)/g' src/*.sv This needs to be followed by some manual cleanup. In particular, all NAME_ME occurences need to be replaced with a suitable assertion name. In addition, some assertions were not disabled during reset (and used $error instead of $fatal), which required a slightly modified sed command to match these: sed -zi 's/assert *property[ \t\r\n]*([ \t\r\n]*@(posedge *$[a-zA-Z_][a-zA-Z0-9_]*$)[ \t\r\n]*$[^;]*$[ \t\r\n]*)[ \t\r\n]*else[ \t\r\n]*\$error[ \t\r\n]*([ \t\r\n]*$[^;]*$[ \t\r\n]*);/`ASSERT(NAME_ME, \2, \1, !rst_ni, \3)/g' src/*.sv Again, some instances of redundant parenthesis could be replaced via: sed -i 's/`ASSERT($[^,]*$, ($[^,]*$),/`ASSERT(\1, \2,/g' src/*.sv

Partially reproducible with the following sed command: sed -zi 's/$[a-zA-Z_][a-zA-Z0-9_]*$[ \t\r\n]*:[ \t\r\n]*assert *property[ \t\r\n]*([ \t\r\n]*@(posedge *$[a-zA-Z_][a-zA-Z0-9_]*$)[ \t\r\n]*disable *iff *([~!]$[^)]*$)[ \t\r\n]*$[^;]*$[ \t\r\n]*);/`ASSERT(\1, \4, \2, !\3)/g' src/*.sv Additionally, the following sed command can be used for unnamed variants without a reset: sed -zi 's/assert *property[ \t\r\n]*([ \t\r\n]*@(posedge *$[a-zA-Z_][a-zA-Z0-9_]*$)[ \t\r\n]*$[^;]*$[ \t\r\n]*);/`ASSERT(\NAME_ME, \2, \1, !rst_ni)/g' src/*.sv Requires cleanup. In particular, all occurences of NAME_ME need to be replaced with suitable names for the asserted properties.

Reproducible with the following sed command for named assumes: sed -zi 's/$[a-zA-Z_][a-zA-Z0-9_]*$[ \t\r\n]*:[ \t\r\n]*assume *property[ \t\r\n]*([ \t\r\n]*@(posedge *$[a-zA-Z_][a-zA-Z0-9_]*$)[ \t\r\n]*disable *iff *([~!]$[^)]*$)[ \t\r\n]*$[^;]*$[ \t\r\n]*)[ \t\r\n]*else[ \t\r\n]*\$fatal[ \t\r\n]*(1,[ \t\r\n]*$[^;]*$[ \t\r\n]*);/`ASSUME(\1, \4, \2, !\3, \5)/g' src/*.sv And the following sed command for unnamed assumes without reset and with $error instead of $fatal: sed -zi 's/assume *property[ \t\r\n]*([ \t\r\n]*@(posedge *$[a-zA-Z_][a-zA-Z0-9_]*$)[ \t\r\n]*$[^;]*$[ \t\r\n]*)[ \t\r\n]*else[ \t\r\n]*\$error[ \t\r\n]*([ \t\r\n]*$[^;]*$[ \t\r\n]*);/`ASSUME(NAME_ME, \2, \1, !rst_ni, \3)/g' src/*.sv Requires cleanup to replace NAME_ME with a suitable property name. Redundant parenthesis can be removed with the following command: sed -i 's/`ASSUME($[^,]*$, ($[^,]*$),/`ASSUME(\1, \2,/g' src/*.sv

Mainly reproducible with the following sequence of sed commands: sed -i '/initial begin/,/end/ s/ assert[ \t\r\n]*([ \t\r\n]*$.*$)/`ASSERT_INIT(NAME_ME, \1, /g' src/*.sv sed -zi 's/`ASSERT_INIT($[^,]*$, $[^,]*$,[ \t\r\n]*else[ \t\r\n]*\$fatal[ \t\r\n]*(1,[ \t\r\n]*$[^;]*$;/`ASSERT_INIT(\1, \2, \3/g' src/*.sv Requires some cleanup. In particular, all instances of NAME_ME must be replaced by sensible assertion names.

No sed magic here. This change was done manually.

Mainly reproducible with the following sed command: sed -i 's/initial assert($[^;]*$);/`ASSERT_INIT(NAME_ME, \1)/g' src/*.sv Requires some cleanup. NAME_ME must be replaced with a sensible assertion name.

Again no sed magic, change applied manually.

Assertions are now disabled if SYNTHESIS is defined within the assertions.svh header.

Use $sformatf() to compose a formatted string before passing it as descriptive message to the assertions macros.

Avoid line-length lint warnings by distributing ASSERT macros over multiple lines, in particular moving log messages to the next line and shortening some of the messages.

michael-platzer · 2024-09-30T06:57:10Z

Thanks a lot @colluca and @phsauter for the reviews!

One thing I would perhaps change, is to move all include statements at the beginning of the files, rather than within the modules. I believe this is more consistent with other include statements and better aligned with one's expectation on where to find included files. Also, for files defining multiple modules e.g. cdc_2phase_clearable this would mean we only need to include it once.

Agree, for the assertion macros this makes more sense, since they are intended to be defined globally anyways.

Could we also move COMMON_CELLS_ASSERTS_OFF to assertions.svh for consistency? As of now, some but not all assertions would be disabled, which I think would go against expectation.

We could, but IMHO that is not consistent and would defeat the purpose to disable assertions in the common_cells sources only while allowing the assertion macros to be used in other places as well. See my comments above.

Finally, in the PR description (and later in the changelog) I would mention that some assertions which did not define a disable iff condition now do after aligning them to use the ASSERT macro, and I would list the files affected by this change (e.g. stream_to_mem.sv).

Good point, will add that.

michael-platzer · 2024-09-30T09:48:18Z

With the help of sed I have identified that only stream_intf.sv and stream_to_mem.sv contain assertions that previously did not use disable iff (or some equivalent default disable statement) and do now due to the switch to the assertion macros. This also made me realize that the stream_intf has no reset port. I have substituted the !rst_ni with 1'b0 to keep the assertions always enabled, which should be equivalent to the previous behavior.

The compiled list of changes that could be added to next release changelog is as follows:

stream_to_mem: Assertions are now disabled during reset.
addr_decode_dync: $warning on assertion violation has been promoted to $error.
cdc_fifo_gray_clearable: $warning on assertion violation has been promoted to $error.
multiaddr_decode: $warning on assertion violation has been promoted to $error.
spill_register_flushable: $warning on assertion violation has been promoted to $error.
rr_arb_tree: Default assertions disable (default disable iff (~rst_ni);) has been removed in favor of disable iff on each assertion.
stream_omega_net: Default assertions disable (default disable iff (~rst_ni);) has been removed in favor of disable iff on each assertion.
stream_xbar: Default assertions disable (default disable iff (~rst_ni);) has been removed in favor of disable iff on each assertion.

michael-platzer · 2024-09-30T11:23:24Z

Please note that addr_decode_dync.sv fails to elaborate with the newest Verilator release 5.028 because of issues with the assertion constructs that are unrelated to the changes in this PR. See #229 (comment)

niwis

Thank you very much @michael-platzer! Also @colluca and @phsauter for your thorough reviews! As far as I can tell, all changes are backwards-compatible. In particular, no new fatals were introduced. Could you confirm? In that case, I think this does not require a major release. Please let me know if you have any objections.

michael-platzer · 2024-10-03T06:57:42Z

As far as I can tell, all changes are backwards-compatible.

To the best of my knowledge, they should be.

In particular, no new fatals were introduced.

That, I can confirm with certainty. Some $fatals have been converted to $errors but there are no new $fatals for sure.

michael-platzer added 4 commits September 18, 2024 08:04

assertions: Rename defines for consistency

1df4e91

assertions: Enable in Verilator by default, disable with global ASSER…

a4ab123

…TS_OFF

assertions: Allow overriding any defines that turn asserts off

b90413c

assertions: Undefine helper macros at end of header

6128757

michael-platzer force-pushed the michael-platzer/feature/use-assert-macros branch 3 times, most recently from a255334 to edcce0a Compare September 18, 2024 15:07

colluca requested changes Sep 26, 2024

View reviewed changes

include/common_cells/assertions.svh Outdated Show resolved Hide resolved

src/stream_omega_net.sv Outdated Show resolved Hide resolved

niwis requested review from niwis, phsauter and WRoenninger September 27, 2024 12:42

phsauter requested changes Sep 27, 2024

View reviewed changes

src/addr_decode_dync.sv Show resolved Hide resolved

src/onehot_to_bin.sv Outdated Show resolved Hide resolved

src/rr_arb_tree.sv Outdated Show resolved Hide resolved

src/rr_arb_tree.sv Outdated Show resolved Hide resolved

src/mem_to_banks_detailed.sv Outdated Show resolved Hide resolved

michael-platzer added 16 commits September 30, 2024 06:51

assertions: Add optional description msg arg to all assert macros

c978a9e

Include assertions.svh header in all sources using assertions

e55f24d

Partially reproducible with the following sed command: sed -zi 's/\nmodule/\n`include "common_cells\/assertions.svh"\n\nmodule/g' `grep assert src/*.sv` Requires extensive cleanup.

Replace final assertion with ASSERT_FINAL macro

0e1e16c

No sed magic here. This change was done manually.

Replace initial assertions with ASSERT_INIT macro

eeef8fd

Mainly reproducible with the following sed command: sed -i 's/initial assert($[^;]*$);/`ASSERT_INIT(NAME_ME, \1)/g' src/*.sv Requires some cleanup. NAME_ME must be replaced with a sensible assertion name.

Replace all immediate assumes with ASSUME_I macro

b4ecb95

Again no sed magic, change applied manually.

Remove unnecessary ifndefs for SYNTHESIS around assertions

de574b8

Assertions are now disabled if SYNTHESIS is defined within the assertions.svh header.

spill_register_flushable: Promote flush+feed warning to error

eb08c3f

Remove obsolete default disables for assertions

8e117dc

addr_decode_dync: Promote onehot assert warning to error

35b6a64

stream_omega_net: Use $sformatf() for assert msg

f543c00

Use $sformatf() to compose a formatted string before passing it as descriptive message to the assertions macros.

stream_xbar: Use $sformatf() for assert msg

d7c357d

Use $sformatf() to compose a formatted string before passing it as descriptive message to the assertions macros.

michael-platzer added 3 commits September 30, 2024 06:51

Distribute ASSERT macros over multiple lines

0a5647a

Avoid line-length lint warnings by distributing ASSERT macros over multiple lines, in particular moving log messages to the next line and shortening some of the messages.

stream_omega_net: Fix typo in assert name

647ec7d

mem_to_banks_detailed: Check power of 2 in a more sensible way

ed55c2a

michael-platzer force-pushed the michael-platzer/feature/use-assert-macros branch from edcce0a to ed55c2a Compare September 30, 2024 06:53

colluca approved these changes Sep 30, 2024

View reviewed changes

michael-platzer requested a review from phsauter September 30, 2024 09:48

phsauter approved these changes Sep 30, 2024

View reviewed changes

michael-platzer added 2 commits October 1, 2024 09:58

stream_intf: Replace non-existing reset with constant in asserts

5b66e85

stream_inft: Add missing include of assertions.svh

f69ec8d

michael-platzer force-pushed the michael-platzer/feature/use-assert-macros branch from 17746ff to f69ec8d Compare October 1, 2024 09:59

niwis approved these changes Oct 3, 2024

View reviewed changes

niwis merged commit a554944 into pulp-platform:master Oct 4, 2024
5 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Replace all asserts & assumes with macros from `assertions.svh` #233

Replace all asserts & assumes with macros from `assertions.svh` #233

michael-platzer commented Sep 18, 2024 •

edited

Loading

colluca commented Sep 18, 2024

michael-platzer commented Sep 24, 2024

colluca left a comment

michael-platzer commented Sep 30, 2024

michael-platzer commented Sep 30, 2024

michael-platzer commented Sep 30, 2024

niwis left a comment

michael-platzer commented Oct 3, 2024

Replace all asserts & assumes with macros from assertions.svh #233

Replace all asserts & assumes with macros from assertions.svh #233

Conversation

michael-platzer commented Sep 18, 2024 • edited Loading

colluca commented Sep 18, 2024

michael-platzer commented Sep 24, 2024

colluca left a comment

Choose a reason for hiding this comment

michael-platzer commented Sep 30, 2024

michael-platzer commented Sep 30, 2024

michael-platzer commented Sep 30, 2024

niwis left a comment

Choose a reason for hiding this comment

michael-platzer commented Oct 3, 2024

Replace all asserts & assumes with macros from `assertions.svh` #233

Replace all asserts & assumes with macros from `assertions.svh` #233

michael-platzer commented Sep 18, 2024 •

edited

Loading