Skip to content

Commit

Permalink
Replace all asserts & assumes with macros from assertions.svh (#233)
Browse files Browse the repository at this point in the history
* assertions: Rename defines for consistency

* assertions: Enable in Verilator by default, disable with global ASSERTS_OFF

* assertions: Allow overriding any defines that turn asserts off

* assertions: Undefine helper macros at end of header

* assertions: Add optional description msg arg to all assert macros

* Include assertions.svh header in all sources using assertions

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 all named concurrent assertions with ASSERT macro

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

* 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

* Replace concurrent assertions without message with ASSERT macro

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.

* 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

* Replace all immediate asserts in initial blocks with ASSERT_INIT macro

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.

* Replace final assertion with ASSERT_FINAL macro

No sed magic here.  This change was done manually.

* Replace initial assertions with ASSERT_INIT macro

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

Again no sed magic, change applied manually.

* Remove unnecessary ifndefs for SYNTHESIS around assertions

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

* spill_register_flushable: Promote flush+feed warning to error

* Remove obsolete default disables for assertions

* addr_decode_dync: Promote onehot assert warning to error

* stream_omega_net: Use $sformatf() for assert msg

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

* stream_xbar: Use $sformatf() for assert msg

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

* Distribute ASSERT macros over multiple lines

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

* mem_to_banks_detailed: Check power of 2 in a more sensible way

* stream_intf: Replace non-existing reset with constant in asserts

* stream_inft: Add missing include of assertions.svh
  • Loading branch information
michael-platzer authored Oct 4, 2024
1 parent b7297b0 commit a554944
Show file tree
Hide file tree
Showing 30 changed files with 297 additions and 394 deletions.
153 changes: 84 additions & 69 deletions include/common_cells/assertions.svh
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
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_comb 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
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

0 comments on commit a554944

Please sign in to comment.