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 all commits
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
153 changes: 84 additions & 69 deletions include/common_cells/assertions.svh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,8 @@
// - Provides default clk and rst options to simplify code
// - Provides boiler plate template for common assertions

`ifndef PRIM_ASSERT_SV
`define PRIM_ASSERT_SV
`ifndef COMMON_CELLS_ASSERTIONS_SVH
`define COMMON_CELLS_ASSERTIONS_SVH

`ifdef UVM
// report assertion error with UVM if compiled
Expand All @@ -25,24 +25,32 @@
///////////////////

// local helper macro to reduce code clutter. undefined at the end of this file
`ifndef VERILATOR
`ifndef ASSERTS_OFF
`ifndef SYNTHESIS
`ifndef XSIM
`define INC_ASSERT
`endif
`endif
`endif
// forcefully enable assertions with ASSERTS_OVERRIDE_ON, overriding any define that turns them off
`ifdef ASSERTS_OVERRIDE_ON
`ifndef INC_ASSERT
`define INC_ASSERT
`endif
`endif

// Converts an arbitrary block of code into a Verilog string
`define PRIM_STRINGIFY(__x) `"__x`"
`define ASSERT_STRINGIFY(__x) `"__x`"

// ASSERT_RPT is available to change the reporting mechanism when an assert fails
`define ASSERT_RPT(__name) \
`ifdef UVM \
assert_rpt_pkg::assert_rpt($sformatf("[%m] %s (%s:%0d)", \
__name, `__FILE__, `__LINE__)); \
`else \
$error("[ASSERT FAILED] [%m] %s (%s:%0d)", __name, `__FILE__, `__LINE__); \
`ifndef ASSERT_RPT
`define ASSERT_RPT(__name, __desc = "") \
`ifdef UVM \
assert_rpt_pkg::assert_rpt($sformatf("[%m] %s: %s (%s:%0d)", \
__name, __desc, `__FILE__, `__LINE__)); \
`else \
$error("[ASSERT FAILED] [%m] %s: %s (%s:%0d)", __name, __desc, `__FILE__, `__LINE__); \
`endif
`endif

///////////////////////////////////////
Expand All @@ -55,66 +63,66 @@

// Immediate assertion
// Note that immediate assertions are sensitive to simulation glitches.
`define ASSERT_I(__name, __prop) \
`ifdef INC_ASSERT \
__name: assert (__prop) \
else begin \
`ASSERT_RPT(`PRIM_STRINGIFY(__name)) \
end \
`define ASSERT_I(__name, __prop, __desc = "") \
`ifdef INC_ASSERT \
__name: assert (__prop) \
else begin \
`ASSERT_RPT(`ASSERT_STRINGIFY(__name), __desc) \
end \
`endif

// Assertion in initial block. Can be used for things like parameter checking.
`define ASSERT_INIT(__name, __prop) \
`ifdef INC_ASSERT \
initial begin \
__name: assert (__prop) \
else begin \
`ASSERT_RPT(`PRIM_STRINGIFY(__name)) \
end \
end \
`define ASSERT_INIT(__name, __prop, __desc = "") \
`ifdef INC_ASSERT \
initial begin \
__name: assert (__prop) \
else begin \
`ASSERT_RPT(`ASSERT_STRINGIFY(__name), __desc) \
end \
end \
`endif

// Assertion in final block. Can be used for things like queues being empty
// at end of sim, all credits returned at end of sim, state machines in idle
// at end of sim.
`define ASSERT_FINAL(__name, __prop) \
`define ASSERT_FINAL(__name, __prop, __desc = "") \
`ifdef INC_ASSERT \
final begin \
__name: assert (__prop || $test$plusargs("disable_assert_final_checks")) \
else begin \
`ASSERT_RPT(`PRIM_STRINGIFY(__name)) \
`ASSERT_RPT(`ASSERT_STRINGIFY(__name), __desc) \
end \
end \
`endif

// 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 begin \
`ASSERT_RPT(`PRIM_STRINGIFY(__name)) \
end \
`define ASSERT(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST, __desc = "") \
`ifdef INC_ASSERT \
__name: assert property (@(posedge __clk) disable iff ((__rst) !== '0) (__prop)) \
else begin \
`ASSERT_RPT(`ASSERT_STRINGIFY(__name), __desc) \
end \
`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.

// Assert a concurrent property NEVER happens
`define ASSERT_NEVER(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \
`ifdef INC_ASSERT \
__name: assert property (@(posedge __clk) disable iff ((__rst) !== '0) not (__prop)) \
else begin \
`ASSERT_RPT(`PRIM_STRINGIFY(__name)) \
end \
`define ASSERT_NEVER(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST, __desc = "") \
`ifdef INC_ASSERT \
__name: assert property (@(posedge __clk) disable iff ((__rst) !== '0) not (__prop)) \
else begin \
`ASSERT_RPT(`ASSERT_STRINGIFY(__name), __desc) \
end \
`endif

// Assert that signal has a known value (each bit is either '0' or '1') after reset.
// It can be called as a module (or interface) body item.
`define ASSERT_KNOWN(__name, __sig, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \
`ifdef INC_ASSERT \
`ASSERT(__name, !$isunknown(__sig), __clk, __rst) \
`define ASSERT_KNOWN(__name, __sig, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST, __desc = "") \
`ifdef INC_ASSERT \
`ASSERT(__name, !$isunknown(__sig), __clk, __rst, __desc) \
`endif

// Cover a concurrent property
Expand All @@ -128,46 +136,46 @@
//////////////////////////////

// Assert that signal is an active-high pulse with pulse length of 1 clock cycle
`define ASSERT_PULSE(__name, __sig, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \
`ifdef INC_ASSERT \
`ASSERT(__name, $rose(__sig) |=> !(__sig), __clk, __rst) \
`define ASSERT_PULSE(__name, __sig, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST, __desc = "") \
`ifdef INC_ASSERT \
`ASSERT(__name, $rose(__sig) |=> !(__sig), __clk, __rst, __desc) \
`endif

// Assert that a property is true only when an enable signal is set. It can be called as a module
// (or interface) body item.
`define ASSERT_IF(__name, __prop, __enable, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \
`ifdef INC_ASSERT \
`ASSERT(__name, (__enable) |-> (__prop), __clk, __rst) \
`define ASSERT_IF(__name, __prop, __enable, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST, __desc = "") \
`ifdef INC_ASSERT \
`ASSERT(__name, (__enable) |-> (__prop), __clk, __rst, __desc) \
`endif

// Assert that signal has a known value (each bit is either '0' or '1') after reset if enable is
// set. It can be called as a module (or interface) body item.
`define ASSERT_KNOWN_IF(__name, __sig, __enable, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \
`define ASSERT_KNOWN_IF(__name, __sig, __enable, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST, __desc = "") \
`ifdef INC_ASSERT \
`ASSERT_KNOWN(__name``KnownEnable, __enable, __clk, __rst) \
`ASSERT_IF(__name, !$isunknown(__sig), __enable, __clk, __rst) \
`ASSERT_KNOWN(__name``KnownEnable, __enable, __clk, __rst, __desc) \
`ASSERT_IF(__name, !$isunknown(__sig), __enable, __clk, __rst, __desc) \
`endif

///////////////////////
// Assumption macros //
///////////////////////

// Assume a concurrent property
`define ASSUME(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \
`ifdef INC_ASSERT \
__name: assume property (@(posedge __clk) disable iff ((__rst) !== '0) (__prop)) \
else begin \
`ASSERT_RPT(`PRIM_STRINGIFY(__name)) \
end \
`define ASSUME(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST, __desc = "") \
`ifdef INC_ASSERT \
__name: assume property (@(posedge __clk) disable iff ((__rst) !== '0) (__prop)) \
else begin \
`ASSERT_RPT(`ASSERT_STRINGIFY(__name), __desc) \
end \
`endif

// Assume an immediate property
`define ASSUME_I(__name, __prop) \
`ifdef INC_ASSERT \
__name: assume (__prop) \
else begin \
`ASSERT_RPT(`PRIM_STRINGIFY(__name)) \
end \
`define ASSUME_I(__name, __prop, __desc = "") \
`ifdef INC_ASSERT \
__name: assume (__prop) \
else begin \
`ASSERT_RPT(`ASSERT_STRINGIFY(__name), __desc) \
end \
`endif

//////////////////////////////////
Expand All @@ -179,16 +187,16 @@

// ASSUME_FPV
// Assume a concurrent property during formal verification only.
`define ASSUME_FPV(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \
`ifdef FPV_ON \
`ASSUME(__name, __prop, __clk, __rst) \
`define ASSUME_FPV(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST, __desc = "") \
`ifdef FPV_ON \
`ASSUME(__name, __prop, __clk, __rst, __desc) \
`endif

// ASSUME_I_FPV
// Assume a concurrent property during formal verification only.
`define ASSUME_I_FPV(__name, __prop) \
`ifdef FPV_ON \
`ASSUME_I(__name, __prop) \
`define ASSUME_I_FPV(__name, __prop, __desc = "") \
`ifdef FPV_ON \
`ASSUME_I(__name, __prop, __desc) \
`endif

// COVER_FPV
Expand All @@ -198,4 +206,11 @@
`COVER(__name, __prop, __clk, __rst) \
`endif

`endif // PRIM_ASSERT_SV

// undefine local helper macros
`ifdef INC_ASSERT
`undef INC_ASSERT
`endif
`undef ASSERT_STRINGIFY

`endif // COMMON_CELLS_ASSERTIONS_SVH
44 changes: 20 additions & 24 deletions src/addr_decode_dync.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@
// - Michael Rogenmoser <[email protected]>
// - Thomas Benz <[email protected]>

`include "common_cells/assertions.svh"

/// Address Decoder: Maps the input address combinatorially to an index.
/// DYNamic Configuration (DYNC) version
/// The address map `addr_map_i` is a packed array of rule_t structs.
Expand Down Expand Up @@ -123,20 +125,16 @@ module addr_decode_dync #(

// Assumptions and assertions
`ifndef COMMON_CELLS_ASSERTS_OFF
`ifndef XSIM
`ifndef SYNTHESIS
initial begin : proc_check_parameters
assume ($bits(addr_i) == $bits(addr_map_i[0].start_addr)) else
$warning($sformatf("Input address has %d bits and address map has %d bits.",
$bits(addr_i), $bits(addr_map_i[0].start_addr)));
assume (NoRules > 0) else
$fatal(1, $sformatf("At least one rule needed"));
assume (NoIndices > 0) else
$fatal(1, $sformatf("At least one index needed"));
`ASSUME_I(addr_width_mismatch, $bits(addr_i) == $bits(addr_map_i[0].start_addr),
$sformatf("Input address has %d bits and address map has %d bits.",
$bits(addr_i), $bits(addr_map_i[0].start_addr)))
`ASSUME_I(norules_0, NoRules > 0, $sformatf("At least one rule needed"))
`ASSUME_I(noindices_0, NoIndices > 0, $sformatf("At least one index needed"))
end

assert final ($onehot0(matched_rules) || config_ongoing_i) else
$warning("More than one bit set in the one-hot signal, matched_rules");
`ASSERT_FINAL(more_than_1_bit_set, $onehot0(matched_rules) || config_ongoing_i,
"More than one bit set in the one-hot signal, matched_rules")

// These following assumptions check the validity of the address map.
// The assumptions gets generated for each distinct pair of rules.
Expand All @@ -149,43 +147,41 @@ module addr_decode_dync #(
always @(addr_map_i or config_ongoing_i) #0 begin : proc_check_addr_map
if (!$isunknown(addr_map_i) && ~config_ongoing_i) begin
for (int unsigned i = 0; i < NoRules; i++) begin
check_start : assume (Napot || addr_map_i[i].start_addr < addr_map_i[i].end_addr ||
addr_map_i[i].end_addr == '0) else
$fatal(1, $sformatf("This rule has a higher start than end address!!!\n\
`ASSUME_I(check_start, Napot || addr_map_i[i].start_addr < addr_map_i[i].end_addr ||
addr_map_i[i].end_addr == '0,
$sformatf("This rule has a higher start than end address!!!\n\
Violating rule %d.\n\
Rule> IDX: %h START: %h END: %h\n\
#####################################################",
i ,addr_map_i[i].idx, addr_map_i[i].start_addr, addr_map_i[i].end_addr));
i ,addr_map_i[i].idx, addr_map_i[i].start_addr, addr_map_i[i].end_addr))
// check the SLV ids
check_idx : assume (addr_map_i[i].idx < NoIndices) else
$fatal(1, $sformatf("This rule has a IDX that is not allowed!!!\n\
`ASSUME_I(check_idx, addr_map_i[i].idx < NoIndices,
$sformatf("This rule has a IDX that is not allowed!!!\n\
Violating rule %d.\n\
Rule> IDX: %h START: %h END: %h\n\
Rule> MAX_IDX: %h\n\
#####################################################",
i, addr_map_i[i].idx, addr_map_i[i].start_addr, addr_map_i[i].end_addr,
(NoIndices-1)));
(NoIndices-1)))
for (int unsigned j = i + 1; j < NoRules; j++) begin
// overlap check
check_overlap : assume (Napot ||
`ASSUME_I(check_overlap, Napot ||
!((addr_map_i[j].start_addr < addr_map_i[i].end_addr) &&
(addr_map_i[j].end_addr > addr_map_i[i].start_addr)) ||
!((addr_map_i[i].end_addr == '0) &&
(addr_map_i[j].end_addr > addr_map_i[i].start_addr)) ||
!((addr_map_i[j].start_addr < addr_map_i[i].end_addr) &&
(addr_map_i[j].end_addr == '0))) else
$warning($sformatf("Overlapping address region found!!!\n\
(addr_map_i[j].end_addr == '0)),
$sformatf("Overlapping address region found!!!\n\
Rule %d: IDX: %h START: %h END: %h\n\
Rule %d: IDX: %h START: %h END: %h\n\
#####################################################",
i, addr_map_i[i].idx, addr_map_i[i].start_addr, addr_map_i[i].end_addr,
j, addr_map_i[j].idx, addr_map_i[j].start_addr, addr_map_i[j].end_addr));
j, addr_map_i[j].idx, addr_map_i[j].start_addr, addr_map_i[j].end_addr))
end
end
end
end
`endif
`endif
`endif

endmodule
10 changes: 5 additions & 5 deletions src/cb_filter.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,8 @@
// - `filter_empty_o`: Filter is empty.
// - `filter_error_o`: One of the internal counters or buckets overflowed.

`include "common_cells/assertions.svh"

/// This is a counting bloom filter
module cb_filter #(
parameter int unsigned KHashes = 32'd3, // Number of hash functions
Expand Down Expand Up @@ -237,12 +239,10 @@ module hash_block #(

`ifndef COMMON_CELLS_ASSERTS_OFF
// assertions
`ifndef SYNTHESIS
initial begin
hash_conf: assume (InpWidth > HashWidth) else
$fatal(1, "%m:\nA Hash Function reduces the width of the input>\nInpWidth: %s\nOUT_WIDTH: %s",
InpWidth, HashWidth);
`ASSUME_I(hash_conf, InpWidth > HashWidth,
$sformatf("%m:\nA Hash Function reduces the width of the input>\nInpWidth: %s\nOUT_WIDTH: %s",
InpWidth, HashWidth))
end
`endif
`endif
endmodule
Loading