Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
niwis merged 25 commits into from
Oct 4, 2024
Merged

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

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
1df4e91
assertions: Rename defines for consistency
michael-platzer Sep 18, 2024
a4ab123
assertions: Enable in Verilator by default, disable with global ASSER…
michael-platzer Sep 18, 2024
b90413c
assertions: Allow overriding any defines that turn asserts off
michael-platzer Sep 18, 2024
6128757
assertions: Undefine helper macros at end of header
michael-platzer Sep 18, 2024
c978a9e
assertions: Add optional description msg arg to all assert macros
michael-platzer Sep 18, 2024
e55f24d
Include assertions.svh header in all sources using assertions
michael-platzer Sep 30, 2024
3565379
Replace all named concurrent assertions with ASSERT macro
michael-platzer Sep 18, 2024
a96c2ad
Replace unnamed concurrent assertions with ASSERT macro
michael-platzer Sep 18, 2024
8a6d004
Replace concurrent assertions without message with ASSERT macro
michael-platzer Sep 18, 2024
1093b48
Replace all concurrent assumes with ASSUME macro
michael-platzer Sep 18, 2024
0a0ec7e
Replace all immediate asserts in initial blocks with ASSERT_INIT macro
michael-platzer Sep 18, 2024
0e1e16c
Replace final assertion with ASSERT_FINAL macro
michael-platzer Sep 18, 2024
eeef8fd
Replace initial assertions with ASSERT_INIT macro
michael-platzer Sep 18, 2024
b4ecb95
Replace all immediate assumes with ASSUME_I macro
michael-platzer Sep 18, 2024
de574b8
Remove unnecessary ifndefs for SYNTHESIS around assertions
michael-platzer Sep 18, 2024
eb08c3f
spill_register_flushable: Promote flush+feed warning to error
michael-platzer Sep 18, 2024
8e117dc
Remove obsolete default disables for assertions
michael-platzer Sep 18, 2024
35b6a64
addr_decode_dync: Promote onehot assert warning to error
michael-platzer Sep 18, 2024
f543c00
stream_omega_net: Use $sformatf() for assert msg
michael-platzer Sep 18, 2024
d7c357d
stream_xbar: Use $sformatf() for assert msg
michael-platzer Sep 18, 2024
0a5647a
Distribute ASSERT macros over multiple lines
michael-platzer Sep 30, 2024
647ec7d
stream_omega_net: Fix typo in assert name
michael-platzer Sep 30, 2024
ed55c2a
mem_to_banks_detailed: Check power of 2 in a more sensible way
michael-platzer Sep 30, 2024
5b66e85
stream_intf: Replace non-existing reset with constant in asserts
michael-platzer Sep 30, 2024
f69ec8d
stream_inft: Add missing include of assertions.svh
michael-platzer Oct 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Replace unnamed concurrent assertions with ASSERT macro 
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
  • Loading branch information
@michael-platzer
michael-platzer committed Sep 30, 2024
commit a96c2ad2465874c8913dc27c7c874ba0ab463c77
6 changes: 2 additions & 4 deletions src/isochronous_4phase_handshake.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,10 +72,8 @@ module isochronous_4phase_handshake (
`ifndef SYNTHESIS
// stability guarantees
`ifndef COMMON_CELLS_ASSERTS_OFF
assert property (@(posedge src_clk_i) disable iff (~src_rst_ni)
(src_valid_i && !src_ready_o |=> $stable(src_valid_i))) else $error("src_valid_i is unstable");
assert property (@(posedge dst_clk_i) disable iff (~dst_rst_ni)
(dst_valid_o && !dst_ready_i |=> $stable(dst_valid_o))) else $error("dst_valid_o is unstable");
`ASSERT(src_valid_unstable, src_valid_i && !src_ready_o |=> $stable(src_valid_i), src_clk_i, !src_rst_ni, "src_valid_i is unstable")
`ASSERT(dst_valid_unstable, dst_valid_o && !dst_ready_i |=> $stable(dst_valid_o), dst_clk_i, !dst_rst_ni, "dst_valid_o is unstable")
`endif
`endif

Expand Down
12 changes: 4 additions & 8 deletions src/isochronous_spill_register.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,14 +99,10 @@ module isochronous_spill_register #(
`ifndef SYNTHESIS
// stability guarantees
`ifndef COMMON_CELLS_ASSERTS_OFF
assert property (@(posedge src_clk_i) disable iff (~src_rst_ni)
(src_valid_i && !src_ready_o |=> $stable(src_valid_i))) else $error("src_valid_i is unstable");
assert property (@(posedge src_clk_i) disable iff (~src_rst_ni)
(src_valid_i && !src_ready_o |=> $stable(src_data_i))) else $error("src_data_i is unstable");
assert property (@(posedge dst_clk_i) disable iff (~dst_rst_ni)
(dst_valid_o && !dst_ready_i |=> $stable(dst_valid_o))) else $error("dst_valid_o is unstable");
assert property (@(posedge dst_clk_i) disable iff (~dst_rst_ni)
(dst_valid_o && !dst_ready_i |=> $stable(dst_data_o))) else $error("dst_data_o is unstable");
`ASSERT(src_valid_unstable, src_valid_i && !src_ready_o |=> $stable(src_valid_i), src_clk_i, !src_rst_ni, "src_valid_i is unstable")
`ASSERT(src_data_unstable, src_valid_i && !src_ready_o |=> $stable(src_data_i), src_clk_i, !src_rst_ni, "src_data_i is unstable")
`ASSERT(dst_valid_unstable, dst_valid_o && !dst_ready_i |=> $stable(dst_valid_o), dst_clk_i, !dst_rst_ni, "dst_valid_o is unstable")
`ASSERT(dst_data_unstable, dst_valid_o && !dst_ready_i |=> $stable(dst_data_o), dst_clk_i, !dst_rst_ni, "dst_data_o is unstable")
`endif
`endif
endmodule
28 changes: 7 additions & 21 deletions src/stream_omega_net.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -272,33 +272,19 @@ module stream_omega_net #(
default disable iff (~rst_ni);
`endif
for (genvar i = 0; unsigned'(i) < NumInp; i++) begin : gen_sel_assertions
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_i[i] |-> sel_i[i] < NumOut)) else
$fatal(1, "Non-existing output is selected!");
`ASSERT(non_existing_output, valid_i[i] |-> sel_i[i] < NumOut, clk_i, !rst_ni, "Non-existing output is selected!")
end

if (AxiVldRdy) begin : gen_handshake_assertions
for (genvar i = 0; unsigned'(i) < NumInp; i++) begin : gen_inp_assertions
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_i[i] && !ready_o[i] |=> $stable(data_i[i] & AxiVldMask))) else
$error("data_i is unstable at input: %0d", i);
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_i[i] && !ready_o[i] |=> $stable(sel_i[i]))) else
$error("sel_i is unstable at input: %0d", i);
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_i[i] && !ready_o[i] |=> valid_i[i])) else
$error("valid_i at input %0d has been taken away without a ready.", i);
`ASSERT(input_data_unstable, valid_i[i] && !ready_o[i] |=> $stable(data_i[i] & AxiVldMask), clk_i, !rst_ni, "data_i is unstable at input: %0d", i)
`ASSERT(input_sel_unstable, valid_i[i] && !ready_o[i] |=> $stable(sel_i[i]), clk_i, !rst_ni, "sel_i is unstable at input: %0d", i)
`ASSERT(input_valid_taken, valid_i[i] && !ready_o[i] |=> valid_i[i], clk_i, !rst_ni, "valid_i at input %0d has been taken away without a ready.", i)
end
for (genvar i = 0; unsigned'(i) < NumOut; i++) begin : gen_out_assertions
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_o[i] && !ready_i[i] |=> $stable(data_o[i] & AxiVldMask))) else
$error("data_o is unstable at output: %0d Check that parameter LockIn is set.", i);
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_o[i] && !ready_i[i] |=> $stable(idx_o[i]))) else
$error("idx_o is unstable at output: %0d Check that parameter LockIn is set.", i);
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_o[i] && !ready_i[i] |=> valid_o[i])) else
$error("valid_o at output %0d has been taken away without a ready.", i);
`ASSERT(output_data_unstable, valid_o[i] && !ready_i[i] |=> $stable(data_o[i] & AxiVldMask), clk_i, !rst_ni, "data_o is unstable at output: %0d Check that parameter LockIn is set.", i)
`ASSERT(output_idx_unstable, valid_o[i] && !ready_i[i] |=> $stable(idx_o[i]), clk_i, !rst_ni, "idx_o is unstable at output: %0d Check that parameter LockIn is set.", i)
`ASSERT(output_valid_taken, valid_o[i] && !ready_i[i] |=> valid_o[i], clk_i, !rst_ni, "valid_o at output %0d has been taken away without a ready.", i)
end
end

Expand Down
9 changes: 3 additions & 6 deletions src/stream_to_mem.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,12 +121,9 @@ module stream_to_mem #(
`ifndef SYNTHESIS
`ifndef COMMON_CELLS_ASSERTS_OFF
if (BufDepth > 0) begin : gen_buf_asserts
assert property (@(posedge clk_i) mem_resp_valid_i |-> buf_ready)
else $error("Memory response lost!");
assert property (@(posedge clk_i) cnt_q == '0 |=> cnt_q != '1)
else $error("Counter underflowed!");
assert property (@(posedge clk_i) cnt_q == BufDepth |=> cnt_q != BufDepth + 1)
else $error("Counter overflowed!");
`ASSERT(memory_response_lost, mem_resp_valid_i |-> buf_ready, clk_i, !rst_ni, "Memory response lost!")
`ASSERT(counter_underflowed, cnt_q == '0 |=> cnt_q != '1, clk_i, !rst_ni, "Counter underflowed!")
`ASSERT(counter_overflowed, cnt_q == BufDepth |=> cnt_q != BufDepth + 1, clk_i, !rst_ni, "Counter overflowed!")
end else begin : gen_no_buf_asserts
assume property (@(posedge clk_i) mem_req_valid_o & mem_req_ready_i |-> mem_resp_valid_i)
else $error("Without BufDepth = 0, the memory must respond in the same cycle!");
Expand Down
28 changes: 7 additions & 21 deletions src/stream_xbar.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -176,33 +176,19 @@ module stream_xbar #(
default disable iff (~rst_ni);
`endif
for (genvar i = 0; unsigned'(i) < NumInp; i++) begin : gen_sel_assertions
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_i[i] |-> sel_i[i] < NumOut)) else
$fatal(1, "Non-existing output is selected!");
`ASSERT(non_existing_output, valid_i[i] |-> sel_i[i] < NumOut, clk_i, !rst_ni, "Non-existing output is selected!")
end

if (AxiVldRdy) begin : gen_handshake_assertions
for (genvar i = 0; unsigned'(i) < NumInp; i++) begin : gen_inp_assertions
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_i[i] && !ready_o[i] |=> $stable(data_i[i] & AxiVldMask))) else
$error("data_i is unstable at input: %0d", i);
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_i[i] && !ready_o[i] |=> $stable(sel_i[i]))) else
$error("sel_i is unstable at input: %0d", i);
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_i[i] && !ready_o[i] |=> valid_i[i])) else
$error("valid_i at input %0d has been taken away without a ready.", i);
`ASSERT(input_data_unstable, valid_i[i] && !ready_o[i] |=> $stable(data_i[i] & AxiVldMask), clk_i, !rst_ni, "data_i is unstable at input: %0d", i)
`ASSERT(input_sel_unstable, valid_i[i] && !ready_o[i] |=> $stable(sel_i[i]), clk_i, !rst_ni, "sel_i is unstable at input: %0d", i)
`ASSERT(input_valid_taken, valid_i[i] && !ready_o[i] |=> valid_i[i], clk_i, !rst_ni, "valid_i at input %0d has been taken away without a ready.", i)
end
for (genvar i = 0; unsigned'(i) < NumOut; i++) begin : gen_out_assertions
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_o[i] && !ready_i[i] |=> $stable(data_o[i] & AxiVldMask))) else
$error("data_o is unstable at output: %0d Check that parameter LockIn is set.", i);
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_o[i] && !ready_i[i] |=> $stable(idx_o[i]))) else
$error("idx_o is unstable at output: %0d Check that parameter LockIn is set.", i);
assert property (@(posedge clk_i) disable iff (~rst_ni)
(valid_o[i] && !ready_i[i] |=> valid_o[i])) else
$error("valid_o at output %0d has been taken away without a ready.", i);
`ASSERT(output_data_unstable, valid_o[i] && !ready_i[i] |=> $stable(data_o[i] & AxiVldMask), clk_i, !rst_ni, "data_o is unstable at output: %0d Check that parameter LockIn is set.", i)
`ASSERT(output_idx_unstable, valid_o[i] && !ready_i[i] |=> $stable(idx_o[i]), clk_i, !rst_ni, "idx_o is unstable at output: %0d Check that parameter LockIn is set.", i)
`ASSERT(output_valid_taken, valid_o[i] && !ready_i[i] |=> valid_o[i], clk_i, !rst_ni, "valid_o at output %0d has been taken away without a ready.", i)
end
end

Expand Down