Skip to content
Merged
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 all concurrent assumes with ASSUME macro
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
  • Loading branch information
michael-platzer committed Sep 30, 2024
commit 1093b48a93ff8b600064a92fb4ecb52c49b4ce7d
4 changes: 1 addition & 3 deletions src/cdc_2phase_clearable.sv
Original file line number Diff line number Diff line change
Expand Up @@ -258,9 +258,7 @@ module cdc_2phase_src_clearable #(
// Assertions
`ifndef COMMON_CELLS_ASSERTS_OFF
`ifndef SYNTHESIS
no_clear_and_request: assume property (
@(posedge clk_i) disable iff(~rst_ni) (clear_i |-> ~valid_i))
else $fatal(1, "No request allowed while clear_i is asserted.");
`ASSUME(no_clear_and_request, clear_i |-> ~valid_i, clk_i, !rst_ni, "No request allowed while clear_i is asserted.")

`endif
`endif
Expand Down
7 changes: 2 additions & 5 deletions src/rr_arb_tree.sv
Original file line number Diff line number Diff line change
Expand Up @@ -179,11 +179,8 @@ module rr_arb_tree #(

logic [NumIn-1:0] req_tmp;
assign req_tmp = req_q & req_i;
lock_req: assume property(
@(posedge clk_i) disable iff (!rst_ni || flush_i)
LockIn |-> lock_d |=> req_tmp == req_q) else
$fatal (1, "It is disallowed to deassert unserved request signals when LockIn is \
enabled.");
`ASSUME(lock_req, LockIn |-> lock_d |=> req_tmp == req_q, clk_i, !rst_ni || flush_i, "It is disallowed to deassert unserved request signals when LockIn is \
enabled.")
`endif
`endif

Expand Down
3 changes: 1 addition & 2 deletions src/stream_to_mem.sv
Original file line number Diff line number Diff line change
Expand Up @@ -125,8 +125,7 @@ module stream_to_mem #(
`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!");
`ASSUME(no_memory_response, mem_req_valid_o & mem_req_ready_i |-> mem_resp_valid_i, clk_i, !rst_ni, "Without BufDepth = 0, the memory must respond in the same cycle!")
end
`endif
`endif
Expand Down