From a55494482fd5488705dbb9c766d1d26992c40592 Mon Sep 17 00:00:00 2001 From: Michael Platzer Date: Fri, 4 Oct 2024 03:03:44 +0200 Subject: [PATCH] Replace all asserts & assumes with macros from `assertions.svh` (#233) * 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 --- include/common_cells/assertions.svh | 153 +++++++++++++++------------- src/addr_decode_dync.sv | 44 ++++---- src/cb_filter.sv | 10 +- src/cdc_2phase_clearable.sv | 13 +-- src/cdc_fifo_2phase.sv | 8 +- src/cdc_fifo_gray.sv | 7 +- src/cdc_fifo_gray_clearable.sv | 7 +- src/exp_backoff.sv | 17 ++-- src/fifo_v3.sv | 18 ++-- src/id_queue.sv | 12 +-- src/isochronous_4phase_handshake.sv | 11 +- src/isochronous_spill_register.sv | 19 ++-- src/lfsr.sv | 31 +++--- src/lfsr_16bit.sv | 10 +- src/lfsr_8bit.sv | 8 +- src/lzc.sv | 15 +-- src/mem_to_banks_detailed.sv | 18 ++-- src/multiaddr_decode.sv | 21 ++-- src/onehot_to_bin.sv | 7 +- src/plru_tree.sv | 13 +-- src/rr_arb_tree.sv | 70 ++++--------- src/spill_register_flushable.sv | 8 +- src/stream_fork.sv | 8 +- src/stream_fork_dynamic.sv | 8 +- src/stream_intf.sv | 8 +- src/stream_join_dynamic.sv | 8 +- src/stream_mux.sv | 8 +- src/stream_omega_net.sv | 60 +++++------ src/stream_to_mem.sv | 22 ++-- src/stream_xbar.sv | 49 ++++----- 30 files changed, 297 insertions(+), 394 deletions(-) diff --git a/include/common_cells/assertions.svh b/include/common_cells/assertions.svh index b6b4b737..1428f97d 100644 --- a/include/common_cells/assertions.svh +++ b/include/common_cells/assertions.svh @@ -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 @@ -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 /////////////////////////////////////// @@ -55,46 +63,46 @@ // 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 @@ -102,19 +110,19 @@ // 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 @@ -128,24 +136,24 @@ ////////////////////////////// // 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 /////////////////////// @@ -153,21 +161,21 @@ /////////////////////// // 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 ////////////////////////////////// @@ -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 @@ -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 diff --git a/src/addr_decode_dync.sv b/src/addr_decode_dync.sv index 37f70083..b0bbb1db 100644 --- a/src/addr_decode_dync.sv +++ b/src/addr_decode_dync.sv @@ -14,6 +14,8 @@ // - Michael Rogenmoser // - Thomas Benz +`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. @@ -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. @@ -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 diff --git a/src/cb_filter.sv b/src/cb_filter.sv index dc2fa9c9..8786defd 100644 --- a/src/cb_filter.sv +++ b/src/cb_filter.sv @@ -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 @@ -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 diff --git a/src/cdc_2phase_clearable.sv b/src/cdc_2phase_clearable.sv index 3367a1f3..c538aa6c 100644 --- a/src/cdc_2phase_clearable.sv +++ b/src/cdc_2phase_clearable.sv @@ -49,6 +49,7 @@ /* verilator lint_off DECLFILENAME */ `include "common_cells/registers.svh" +`include "common_cells/assertions.svh" module cdc_2phase_clearable #( parameter type T = logic, @@ -187,9 +188,7 @@ module cdc_2phase_clearable #( `ifndef COMMON_CELLS_ASSERTS_OFF - no_valid_i_during_clear_i : assert property ( - @(posedge src_clk_i) disable iff (!src_rst_ni) src_clear_i |-> !src_valid_i - ); + `ASSERT(no_valid_i_during_clear_i, src_clear_i |-> !src_valid_i, src_clk_i, !src_rst_ni) `endif @@ -258,12 +257,8 @@ 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."); - - `endif + `ASSUME(no_clear_and_request, clear_i |-> ~valid_i, clk_i, !rst_ni, + "No request allowed while clear_i is asserted.") `endif endmodule diff --git a/src/cdc_fifo_2phase.sv b/src/cdc_fifo_2phase.sv index d482283a..e20c31a4 100644 --- a/src/cdc_fifo_2phase.sv +++ b/src/cdc_fifo_2phase.sv @@ -11,6 +11,8 @@ // // Fabian Schuiki +`include "common_cells/assertions.svh" + /// A clock domain crossing FIFO, using 2-phase hand shakes. /// /// This FIFO has its push and pop ports in two separate clock domains. Its size @@ -62,10 +64,8 @@ module cdc_fifo_2phase #( ); // Check the invariants. - `ifndef SYNTHESIS - initial begin - assert(LOG_DEPTH > 0); - end + `ifndef COMMON_CELLS_ASSERTS_OFF + `ASSERT_INIT(log_depth_0, LOG_DEPTH > 0) `endif localparam int PtrWidth = LOG_DEPTH+1; diff --git a/src/cdc_fifo_gray.sv b/src/cdc_fifo_gray.sv index bca5acc1..a4e3d839 100644 --- a/src/cdc_fifo_gray.sv +++ b/src/cdc_fifo_gray.sv @@ -96,6 +96,7 @@ /// ``` `include "common_cells/registers.svh" +`include "common_cells/assertions.svh" (* no_ungroup *) (* no_boundary_optimization *) @@ -157,11 +158,9 @@ module cdc_fifo_gray #( ); // Check the invariants. - `ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - initial assert(LOG_DEPTH > 0); - initial assert(SYNC_STAGES >= 2); - `endif + `ASSERT_INIT(log_depth_0, LOG_DEPTH > 0) + `ASSERT_INIT(sync_stages_gt_2, SYNC_STAGES >= 2) `endif endmodule diff --git a/src/cdc_fifo_gray_clearable.sv b/src/cdc_fifo_gray_clearable.sv index a7ccea03..69f8015c 100644 --- a/src/cdc_fifo_gray_clearable.sv +++ b/src/cdc_fifo_gray_clearable.sv @@ -96,6 +96,7 @@ /// async] ``` `include "common_cells/registers.svh" +`include "common_cells/assertions.svh" (* no_ungroup *) (* no_boundary_optimization *) @@ -254,11 +255,9 @@ module cdc_fifo_gray_clearable #( assign dst_clear_pending_o = s_dst_isolate_req; // Check the invariants. - `ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - initial assert(LOG_DEPTH > 0); - initial assert(SYNC_STAGES >= 2); - `endif + `ASSERT_INIT(log_depth_0, LOG_DEPTH > 0) + `ASSERT_INIT(sync_stages_lt_2, SYNC_STAGES >= 2) `endif endmodule diff --git a/src/exp_backoff.sv b/src/exp_backoff.sv index 3a970b97..6b098b4b 100644 --- a/src/exp_backoff.sv +++ b/src/exp_backoff.sv @@ -20,6 +20,8 @@ // a successful trial (clr_i). // +`include "common_cells/assertions.svh" + module exp_backoff #( /// Seed for 16bit LFSR parameter int unsigned Seed = 'hffff, @@ -81,18 +83,11 @@ module exp_backoff #( // assertions /////////////////////////////////////////////////////// -`ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - initial begin - // assert wrong parameterizations - assert (MaxExp>0) - else $fatal(1,"MaxExp must be greater than 0"); - assert (MaxExp<=16) - else $fatal(1,"MaxExp cannot be greater than 16"); - assert (Seed>0) - else $fatal(1,"Zero seed is not allowed for LFSR"); - end -`endif + // assert wrong parameterizations + `ASSERT_INIT(max_exp_0, MaxExp>0, "MaxExp must be greater than 0") + `ASSERT_INIT(max_exp_gt_16, MaxExp<=16, "MaxExp cannot be greater than 16") + `ASSERT_INIT(seed_0, Seed>0, "Zero seed is not allowed for LFSR") `endif endmodule // exp_backoff diff --git a/src/fifo_v3.sv b/src/fifo_v3.sv index 83df3b23..a15b8cf6 100644 --- a/src/fifo_v3.sv +++ b/src/fifo_v3.sv @@ -10,6 +10,8 @@ // Author: Florian Zaruba +`include "common_cells/assertions.svh" + module fifo_v3 #( parameter bit FALL_THROUGH = 1'b0, // fifo is in fall-through mode parameter int unsigned DATA_WIDTH = 32, // default data width if the fifo is of type logic @@ -137,20 +139,14 @@ module fifo_v3 #( end end -`ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - initial begin - assert (DEPTH > 0) else $error("DEPTH must be greater than 0."); - end + `ASSERT_INIT(depth_0, DEPTH > 0, "DEPTH must be greater than 0.") - full_write : assert property( - @(posedge clk_i) disable iff (~rst_ni) (full_o |-> ~push_i)) - else $fatal (1, "Trying to push new data although the FIFO is full."); + `ASSERT(full_write, full_o |-> ~push_i, clk_i, !rst_ni, + "Trying to push new data although the FIFO is full.") - empty_read : assert property( - @(posedge clk_i) disable iff (~rst_ni) (empty_o |-> ~pop_i)) - else $fatal (1, "Trying to pop data although the FIFO is empty."); -`endif + `ASSERT(empty_read, empty_o |-> ~pop_i, clk_i, !rst_ni, + "Trying to pop data although the FIFO is empty.") `endif endmodule // fifo_v3 diff --git a/src/id_queue.sv b/src/id_queue.sv index 1737381d..6d9c1763 100644 --- a/src/id_queue.sv +++ b/src/id_queue.sv @@ -45,6 +45,8 @@ // Maintainers: // - Andreas Kurth +`include "common_cells/assertions.svh" + module id_queue #( parameter int ID_WIDTH = 0, parameter int CAPACITY = 0, @@ -410,15 +412,9 @@ module id_queue #( end // Validate parameters. -`ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - initial begin: validate_params - assert (ID_WIDTH >= 1) - else $fatal(1, "The ID must at least be one bit wide!"); - assert (CAPACITY >= 1) - else $fatal(1, "The queue must have capacity of at least one entry!"); - end -`endif + `ASSERT_INIT(id_width_0, ID_WIDTH >= 1, "The ID must at least be one bit wide!") + `ASSERT_INIT(capacity_0, CAPACITY >= 1, "The queue must have capacity of at least one entry!") `endif endmodule diff --git a/src/isochronous_4phase_handshake.sv b/src/isochronous_4phase_handshake.sv index 07786584..2d3e4afd 100644 --- a/src/isochronous_4phase_handshake.sv +++ b/src/isochronous_4phase_handshake.sv @@ -39,6 +39,7 @@ /// ratio will work. `include "common_cells/registers.svh" +`include "common_cells/assertions.svh" module isochronous_4phase_handshake ( input logic src_clk_i, @@ -68,14 +69,12 @@ module isochronous_4phase_handshake ( // destination is valid if we didn't yet get acknowledge assign dst_valid_o = (dst_req_q != dst_ack_q); - `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"); - `endif + `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 endmodule diff --git a/src/isochronous_spill_register.sv b/src/isochronous_spill_register.sv index 6c3048ed..1c2965de 100644 --- a/src/isochronous_spill_register.sv +++ b/src/isochronous_spill_register.sv @@ -12,6 +12,7 @@ // Florian Zaruba `include "common_cells/registers.svh" +`include "common_cells/assertions.svh" /// A register with handshakes that completely cuts any combinatorial paths /// between the input and output in isochronous clock domains. @@ -95,17 +96,15 @@ module isochronous_spill_register #( assign dst_data_o = mem_q[rd_pointer_q[0]]; end - `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"); - `endif + `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 endmodule diff --git a/src/lfsr.sv b/src/lfsr.sv index ed6cb808..0891ed31 100644 --- a/src/lfsr.sv +++ b/src/lfsr.sv @@ -19,6 +19,8 @@ // patterns. The additional cipher layers can only be used for an LFSR width // of 64bit, since the block cipher has been designed for that block length. +`include "common_cells/assertions.svh" + module lfsr #( parameter int unsigned LfsrWidth = 64, // [4,64] parameter int unsigned OutWidth = 8, // [1,LfsrWidth] @@ -290,25 +292,18 @@ end // assertions //////////////////////////////////////////////////////////////////////// `ifndef COMMON_CELLS_ASSERTS_OFF -`ifndef SYNTHESIS -initial begin - // these are the LUT limits - assert(OutWidth <= LfsrWidth) else - $fatal(1,"OutWidth must be smaller equal the LfsrWidth."); - assert(RstVal > unsigned'(0)) else - $fatal(1,"RstVal must be nonzero."); - assert((LfsrWidth >= $low(Masks)) && (LfsrWidth <= $high(Masks))) else - $fatal(1,"Unsupported LfsrWidth."); - assert(Masks[LfsrWidth][LfsrWidth-1]) else - $fatal(1, "LFSR mask is not correct. The MSB must be 1." ); - assert((CipherLayers > 0) && (LfsrWidth == 64) || (CipherLayers == 0)) else - $fatal(1, "Use additional cipher layers only in conjunction with an LFSR width of 64 bit." ); -end +// these are the LUT limits +`ASSERT_INIT(outwidth_gt_lfsrwidth, OutWidth <= LfsrWidth, + "OutWidth must be smaller equal the LfsrWidth.") +`ASSERT_INIT(rstval_0, RstVal > unsigned'(0), "RstVal must be nonzero.") +`ASSERT_INIT(lfsrwidth_invalid, (LfsrWidth >= $low(Masks)) && (LfsrWidth <= $high(Masks)), + "Unsupported LfsrWidth.") +`ASSERT_INIT(mask_invalid, Masks[LfsrWidth][LfsrWidth-1], + "LFSR mask is not correct. The MSB must be 1.") +`ASSERT_INIT(cipherlayers_invalid, (CipherLayers > 0) && (LfsrWidth == 64) || (CipherLayers == 0), + "Use additional cipher layers only in conjunction with an LFSR width of 64 bit.") - all_zero: assert property ( - @(posedge clk_i) disable iff (!rst_ni) en_i |-> lfsr_d) - else $fatal(1,"Lfsr must not be all-zero."); -`endif + `ASSERT(all_zero, en_i |-> lfsr_d, clk_i, !rst_ni, "Lfsr must not be all-zero.") `endif endmodule // lfsr diff --git a/src/lfsr_16bit.sv b/src/lfsr_16bit.sv index 77947c0f..dd29ddad 100644 --- a/src/lfsr_16bit.sv +++ b/src/lfsr_16bit.sv @@ -12,6 +12,8 @@ // Date: 5.11.2018 // Description: 16-bit LFSR +`include "common_cells/assertions.svh" + // -------------- // 16-bit LFSR // -------------- @@ -59,12 +61,8 @@ module lfsr_16bit #( end `ifndef COMMON_CELLS_ASSERTS_OFF - `ifndef SYNTHESIS - initial begin - assert (WIDTH <= 16) - else $fatal(1, "WIDTH needs to be less than 16 because of the 16-bit LFSR"); - end - `endif + `ASSERT_INIT(width_gt_16, WIDTH <= 16, + "WIDTH needs to be less than 16 because of the 16-bit LFSR") `endif endmodule diff --git a/src/lfsr_8bit.sv b/src/lfsr_8bit.sv index ed6ca98a..98ca3a86 100644 --- a/src/lfsr_8bit.sv +++ b/src/lfsr_8bit.sv @@ -13,6 +13,8 @@ // Date: 12.11.2017 // Description: 8-bit LFSR +`include "common_cells/assertions.svh" + /// 8 bit Linear Feedback Shift register module lfsr_8bit #( parameter logic [7:0] SEED = 8'b0, @@ -53,11 +55,7 @@ module lfsr_8bit #( end `ifndef COMMON_CELLS_ASSERTS_OFF - `ifndef SYNTHESIS - initial begin - assert (WIDTH <= 8) else $fatal(1, "WIDTH needs to be less than 8 because of the 8-bit LFSR"); - end - `endif + `ASSERT_INIT(width_gt_8, WIDTH <= 8, "WIDTH needs to be less than 8 because of the 8-bit LFSR") `endif endmodule diff --git a/src/lzc.sv b/src/lzc.sv index f051a665..eccc31a5 100644 --- a/src/lzc.sv +++ b/src/lzc.sv @@ -2,6 +2,8 @@ // Solderpad Hardware License, Version 0.51, see LICENSE for details. // SPDX-License-Identifier: SHL-0.51 +`include "common_cells/assertions.svh" + /// A trailing zero counter / leading zero counter. /// Set MODE to 0 for trailing zero counter => cnt_o is the number of trailing zeros (from the LSB) /// Set MODE to 1 for leading zero counter => cnt_o is the number of leading zeros (from the MSB) @@ -40,11 +42,7 @@ module lzc #( localparam int unsigned NumLevels = $clog2(WIDTH); `ifndef COMMON_CELLS_ASSERTS_OFF - `ifndef SYNTHESIS - initial begin - assert(WIDTH > 0) else $fatal(1, "input must be at least one bit wide"); - end - `endif + `ASSERT_INIT(width_0, WIDTH > 0, "input must be at least one bit wide") `endif logic [WIDTH-1:0][NumLevels-1:0] index_lut; @@ -101,13 +99,8 @@ module lzc #( end : gen_lzc -`ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - initial begin: validate_params - assert (WIDTH >= 1) - else $fatal(1, "The WIDTH must at least be one bit wide!"); - end -`endif + `ASSERT_INIT(width_0, WIDTH >= 1, "The WIDTH must at least be one bit wide!") `endif endmodule : lzc diff --git a/src/mem_to_banks_detailed.sv b/src/mem_to_banks_detailed.sv index 24160031..8255f00d 100644 --- a/src/mem_to_banks_detailed.sv +++ b/src/mem_to_banks_detailed.sv @@ -10,6 +10,8 @@ // // Author: Wolfgang Roenninger +`include "common_cells/assertions.svh" + /// Split memory access over multiple parallel banks, where each bank has its own req/gnt /// request and valid response direction. module mem_to_banks_detailed #( @@ -218,18 +220,14 @@ module mem_to_banks_detailed #( assign rvalid_o = &(resp_valid | dead_response); // Assertions - `ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - `ifndef SYNTHESIS initial begin - assume (DataWidth != 0 && (DataWidth & (DataWidth - 1)) == 0) - else $fatal(1, "Data width must be a power of two!"); - assume (DataWidth % NumBanks == 0) - else $fatal(1, "Data width must be evenly divisible over banks!"); - assume ((DataWidth / NumBanks) % 8 == 0) - else $fatal(1, "Data width of each bank must be divisible into 8-bit bytes!"); + `ASSUME_I(datawidth_not_power_of_2, DataWidth != 0 && 2**$clog2(DataWidth) == DataWidth, + "Data width must be a power of two!") + `ASSUME_I(datawidth_not_divisible_by_banks, DataWidth % NumBanks == 0, + "Data width must be evenly divisible over banks!") + `ASSUME_I(bank_datawidth_not_divisible_by_8, (DataWidth / NumBanks) % 8 == 0, + "Data width of each bank must be divisible into 8-bit bytes!") end `endif - `endif - `endif endmodule diff --git a/src/multiaddr_decode.sv b/src/multiaddr_decode.sv index 61466eab..f73e560a 100644 --- a/src/multiaddr_decode.sv +++ b/src/multiaddr_decode.sv @@ -10,6 +10,8 @@ // Author: Luca Colagrande +`include "common_cells/assertions.svh" + /// Multi-address Decoder: Combinational module which takes an address set /// in {addr, mask} representation and returns a bit mask `select_o` indicating which /// address map rules in `addr_map_i` it matches. @@ -121,14 +123,11 @@ module multiaddr_decode #( // Assumptions and assertions `ifndef COMMON_CELLS_ASSERTS_OFF - `ifndef XSIM - `ifndef SYNTHESIS initial begin : proc_check_parameters - assume (NoRules > 0) else - $fatal(1, $sformatf("At least one rule needed")); - assume ($bits(addr_i) == $bits(addr_map_i[0].addr)) else - $warning($sformatf("Input address has %d bits and address map has %d bits.", - $bits(addr_i), $bits(addr_map_i[0].addr))); + `ASSUME_I(norules_0, NoRules > 0, $sformatf("At least one rule needed")) + `ASSUME_I(addr_width_not_equal, $bits(addr_i) == $bits(addr_map_i[0].addr), + $sformatf("Input address has %d bits and address map has %d bits.", + $bits(addr_i), $bits(addr_map_i[0].addr))) end // These following assumptions check the validity of the address map. @@ -137,18 +136,16 @@ module multiaddr_decode #( if (!$isunknown(addr_map_i)) begin for (int unsigned i = 0; i < NoRules; i++) begin // 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\n\ Rule> MAX_IDX: %h\n\ #####################################################", - i, addr_map_i[i].idx, (NoIndices-1))); + i, addr_map_i[i].idx, (NoIndices-1))) end end end `endif - `endif - `endif endmodule diff --git a/src/onehot_to_bin.sv b/src/onehot_to_bin.sv index 47dae21e..69bf3bcf 100644 --- a/src/onehot_to_bin.sv +++ b/src/onehot_to_bin.sv @@ -10,6 +10,8 @@ // Franceco Conti +`include "common_cells/assertions.svh" + module onehot_to_bin #( parameter int unsigned ONEHOT_WIDTH = 16, // Do Not Change @@ -29,10 +31,7 @@ module onehot_to_bin #( assign bin[j] = |(tmp_mask & onehot); end -`ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - assert final ($onehot0(onehot)) else - $fatal(1, "[onehot_to_bin] More than two bit set in the one-hot signal"); -`endif + `ASSERT_FINAL(more_than_2_bits, $onehot0(onehot), "More than two bit set in the one-hot signal") `endif endmodule diff --git a/src/plru_tree.sv b/src/plru_tree.sv index 3d87578e..21add5a1 100644 --- a/src/plru_tree.sv +++ b/src/plru_tree.sv @@ -14,6 +14,8 @@ // Description: Pseudo Least Recently Used Tree (PLRU) // See: https://en.wikipedia.org/wiki/Pseudo-LRU +`include "common_cells/assertions.svh" + module plru_tree #( parameter int unsigned ENTRIES = 16 ) ( @@ -118,16 +120,11 @@ module plru_tree #( end end -`ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - initial begin - assert (ENTRIES == 2**LogEntries) else $error("Entries must be a power of two"); - end + `ASSERT_INIT(entries_not_power_of_2, ENTRIES == 2**LogEntries, "Entries must be a power of two") - output_onehot : assert property( - @(posedge clk_i) disable iff (~rst_ni) ($onehot0(plru_o))) - else $fatal (1, "More than one bit set in PLRU output."); -`endif + `ASSERT(output_onehot, $onehot0(plru_o), clk_i, !rst_ni, + "More than one bit set in PLRU output.") `endif endmodule diff --git a/src/rr_arb_tree.sv b/src/rr_arb_tree.sv index 1aa566d4..67bf1ce4 100644 --- a/src/rr_arb_tree.sv +++ b/src/rr_arb_tree.sv @@ -13,6 +13,8 @@ // Date: 02.04.2019 // Description: logarithmic arbitration tree with round robin arbitration scheme. +`include "common_cells/assertions.svh" + /// The rr_arb_tree employs non-starving round robin-arbitration - i.e., the priorities /// rotate each cycle. /// @@ -109,17 +111,6 @@ module rr_arb_tree #( output idx_t idx_o ); - `ifndef SYNTHESIS - `ifndef COMMON_CELLS_ASSERTS_OFF - `ifndef VERILATOR - `ifndef XSIM - // Default SVA reset - default disable iff (!rst_ni || flush_i); - `endif - `endif - `endif - `endif - // just pass through in this corner case if (NumIn == unsigned'(1)) begin : gen_pass_through assign req_o = req_i[0]; @@ -170,22 +161,15 @@ module rr_arb_tree #( end end - `ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - lock: assert property( - @(posedge clk_i) disable iff (!rst_ni || flush_i) - LockIn |-> req_o && (!gnt_i && !flush_i) |=> idx_o == $past(idx_o)) else - $fatal (1, "Lock implies same arbiter decision in next cycle if output is not \ - ready."); + `ASSERT(lock, LockIn |-> req_o && (!gnt_i && !flush_i) |=> idx_o == $past(idx_o), + clk_i, !rst_ni || flush_i, + "Lock implies same arbiter decision in next cycle if output is not ready.") 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."); - `endif + `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 always_ff @(posedge clk_i or negedge rst_ni) begin : p_req_regs @@ -310,41 +294,25 @@ module rr_arb_tree #( end end - `ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - `ifndef XSIM - initial begin : p_assert - assert(NumIn) - else $fatal(1, "Input must be at least one element wide."); - assert(!(LockIn && ExtPrio)) - else $fatal(1,"Cannot use LockIn feature together with external ExtPrio."); - end + `ASSERT_INIT(numin_0, NumIn, "Input must be at least one element wide.") + `ASSERT_INIT(lockin_and_extprio, !(LockIn && ExtPrio), + "Cannot use LockIn feature together with external ExtPrio.") - hot_one : assert property( - @(posedge clk_i) disable iff (!rst_ni || flush_i) $onehot0(gnt_o)) - else $fatal (1, "Grant signal must be hot1 or zero."); + `ASSERT(hot_one, $onehot0(gnt_o), clk_i, !rst_ni || flush_i, + "Grant signal must be hot1 or zero.") - gnt0 : assert property( - @(posedge clk_i) disable iff (!rst_ni || flush_i) |gnt_o |-> gnt_i) - else $fatal (1, "Grant out implies grant in."); + `ASSERT(gnt0, |gnt_o |-> gnt_i, clk_i, !rst_ni || flush_i, "Grant out implies grant in.") - gnt1 : assert property( - @(posedge clk_i) disable iff (!rst_ni || flush_i) req_o |-> gnt_i |-> |gnt_o) - else $fatal (1, "Req out and grant in implies grant out."); + `ASSERT(gnt1, req_o |-> gnt_i |-> |gnt_o, clk_i, !rst_ni || flush_i, + "Req out and grant in implies grant out.") - gnt_idx : assert property( - @(posedge clk_i) disable iff (!rst_ni || flush_i) req_o |-> gnt_i |-> gnt_o[idx_o]) - else $fatal (1, "Idx_o / gnt_o do not match."); + `ASSERT(gnt_idx, req_o |-> gnt_i |-> gnt_o[idx_o], clk_i, !rst_ni || flush_i, + "Idx_o / gnt_o do not match.") - req0 : assert property( - @(posedge clk_i) disable iff (!rst_ni || flush_i) |req_i |-> req_o) - else $fatal (1, "Req in implies req out."); + `ASSERT(req0, |req_i |-> req_o, clk_i, !rst_ni || flush_i, "Req in implies req out.") - req1 : assert property( - @(posedge clk_i) disable iff (!rst_ni || flush_i) req_o |-> |req_i) - else $fatal (1, "Req out implies req in."); - `endif - `endif + `ASSERT(req1, req_o |-> |req_i, clk_i, !rst_ni || flush_i, "Req out implies req in.") `endif end diff --git a/src/spill_register_flushable.sv b/src/spill_register_flushable.sv index cea3fc88..7d07adc5 100644 --- a/src/spill_register_flushable.sv +++ b/src/spill_register_flushable.sv @@ -11,6 +11,7 @@ // // Fabian Schuiki +`include "common_cells/assertions.svh" /// A register with handshakes that completely cuts any combinational paths /// between the input and output. This spill register can be flushed. @@ -94,12 +95,9 @@ module spill_register_flushable #( // We empty the spill register before the slice register. assign data_o = b_full_q ? b_data_q : a_data_q; - `ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - flush_valid : assert property ( - @(posedge clk_i) disable iff (~rst_ni) (flush_i |-> ~valid_i)) else - $warning("Trying to flush and feed the spill register simultaneously. You will lose data!"); + `ASSERT(flush_valid, flush_i |-> ~valid_i, clk_i, !rst_ni, + "Trying to flush and feed the spill register simultaneously. You will lose data!") `endif - `endif end endmodule diff --git a/src/stream_fork.sv b/src/stream_fork.sv index f645241d..ebe65f9b 100644 --- a/src/stream_fork.sv +++ b/src/stream_fork.sv @@ -16,6 +16,8 @@ // This module has no data ports because stream data does not need to be forked: the data of the // input stream can just be applied at all output streams. +`include "common_cells/assertions.svh" + module stream_fork #( parameter int unsigned N_OUP = 0 // Synopsys DC requires a default value for parameters. ) ( @@ -122,12 +124,8 @@ module stream_fork #( assign all_ones = '1; // Synthesis fix for Vivado, which does not correctly compute the width // of the '1 literal when assigned to a port of parametrized width. -`ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - initial begin: p_assertions - assert (N_OUP >= 1) else $fatal(1, "Number of outputs must be at least 1!"); - end -`endif + `ASSERT_INIT(n_oup_0, N_OUP >= 1, "Number of outputs must be at least 1!") `endif endmodule diff --git a/src/stream_fork_dynamic.sv b/src/stream_fork_dynamic.sv index baeaf75b..8da5313d 100644 --- a/src/stream_fork_dynamic.sv +++ b/src/stream_fork_dynamic.sv @@ -11,6 +11,8 @@ // Authors: // - Andreas Kurth +`include "common_cells/assertions.svh" + /// Dynamic stream fork: Connects the input stream (ready-valid) handshake to a combination of output /// stream handshake. The combination is determined dynamically through another stream, which /// provides a bitmask for the fork. For each input stream handshake, every output stream handshakes @@ -85,11 +87,7 @@ module stream_fork_dynamic #( .ready_i ( int_oup_ready ) ); -`ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - initial begin: p_assertions - assert (N_OUP >= 1) else $fatal(1, "N_OUP must be at least 1!"); - end -`endif + `ASSERT_INIT(n_oup_0, N_OUP >= 1, "N_OUP must be at least 1!") `endif endmodule diff --git a/src/stream_intf.sv b/src/stream_intf.sv index 1def97fe..23bfde20 100644 --- a/src/stream_intf.sv +++ b/src/stream_intf.sv @@ -11,6 +11,8 @@ // Author: Florian Zaruba +`include "common_cells/assertions.svh" + /// A stream interface with custom payload of type `payload_t`. /// Handshaking rules as defined in the AXI standard. interface STREAM_DV #( @@ -40,10 +42,8 @@ interface STREAM_DV #( ); // Make sure that the handshake and payload is stable - `ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - assert property (@(posedge clk_i) (valid && !ready |=> $stable(data))); - assert property (@(posedge clk_i) (valid && !ready |=> valid)); - `endif + `ASSERT(data_unstable, (valid && !ready |=> $stable(data)), clk_i, 1'b0) + `ASSERT(valid_unstable, (valid && !ready |=> valid), clk_i, 1'b0) `endif endinterface diff --git a/src/stream_join_dynamic.sv b/src/stream_join_dynamic.sv index 16551bee..db874b7f 100644 --- a/src/stream_join_dynamic.sv +++ b/src/stream_join_dynamic.sv @@ -11,6 +11,8 @@ // Authors: // - Luca Colagrande +`include "common_cells/assertions.svh" + // Stream join dynamic: Joins a parametrizable number of input streams (i.e. valid-ready // handshaking with dependency rules as in AXI4) to a single output stream. The subset of streams // to join can be configured dynamically via `sel_i`. The output handshake happens only after @@ -37,11 +39,7 @@ module stream_join_dynamic #( assign inp_ready_o[i] = oup_valid_o & oup_ready_i; end -`ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - initial begin: p_assertions - assert (N_INP >= 1) else $fatal(1, "N_INP must be at least 1!"); - end -`endif + `ASSERT_INIT(n_inp_0, N_INP >= 1, "N_INP must be at least 1!") `endif endmodule diff --git a/src/stream_mux.sv b/src/stream_mux.sv index 90db8bdc..da5c951a 100644 --- a/src/stream_mux.sv +++ b/src/stream_mux.sv @@ -8,6 +8,8 @@ // CONDITIONS OF ANY KIND, either express or implied. See the License for the // specific language governing permissions and limitations under the License. +`include "common_cells/assertions.svh" + /// Stream multiplexer: connects the output to one of `N_INP` data streams with valid-ready /// handshaking. @@ -35,12 +37,8 @@ module stream_mux #( assign oup_data_o = inp_data_i[inp_sel_i]; assign oup_valid_o = inp_valid_i[inp_sel_i]; -`ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - initial begin: p_assertions - assert (N_INP >= 1) else $fatal (1, "The number of inputs must be at least 1!"); - end -`endif + `ASSERT_INIT(n_inp_0, N_INP >= 1, "The number of inputs must be at least 1!") `endif endmodule diff --git a/src/stream_omega_net.sv b/src/stream_omega_net.sv index 224ff1f1..206871f0 100644 --- a/src/stream_omega_net.sv +++ b/src/stream_omega_net.sv @@ -10,6 +10,8 @@ // Author: Wolfgang Roenninger +`include "common_cells/assertions.svh" + /// Omega network using multiple `stream_xbar` as switches. /// /// An omega network is isomorphic to a butterfly network. @@ -264,51 +266,41 @@ module stream_omega_net #( // Assertions // Make sure that the handshake and payload is stable - `ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - `ifndef VERILATOR - 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, $sformatf("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, $sformatf("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, + $sformatf("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, + $sformatf("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, + $sformatf("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, + $sformatf("valid_o at output %0d has been taken away without a ready.", i)) end end - initial begin : proc_parameter_assertions - assert ((2**$clog2(Radix) == Radix) && (Radix > 32'd1)) else - $fatal(1, "Radix %0d is not power of two.", Radix); - assert (2**$clog2(NumRouters) == NumRouters) else - $fatal(1, "NumRouters %0d is not power of two.", NumRouters); - assert ($clog2(NumLanes) % SelW == 0) else - $fatal(1, "Bit slicing of the internal selection signal is broken."); - end - `endif + `ASSERT_INIT(radix_not_power_of_2, (2**$clog2(Radix) == Radix) && (Radix > 32'd1), + "Radix is not power of two.") + `ASSERT_INIT(num_routers_not_power_of_2, 2**$clog2(NumRouters) == NumRouters, + "NumRouters is not power of two.") + `ASSERT_INIT(bit_slicing_broken, $clog2(NumLanes) % SelW == 0, + "Bit slicing of the internal selection signal is broken.") `endif end endmodule diff --git a/src/stream_to_mem.sv b/src/stream_to_mem.sv index 163c33e7..dddc2193 100644 --- a/src/stream_to_mem.sv +++ b/src/stream_to_mem.sv @@ -11,9 +11,11 @@ // Authors: // - Andreas Kurth +`include "common_cells/registers.svh" +`include "common_cells/assertions.svh" + /// `stream_to_mem`: Allows to use memories with flow control (`valid`/`ready`) for requests but without flow /// control for output data to be used in streams. -`include "common_cells/registers.svh" module stream_to_mem #( /// Memory request payload type, usually write enable, write data, etc. parameter type mem_req_t = logic, @@ -116,19 +118,17 @@ module stream_to_mem #( assign mem_req_o = req_i; // Assertions -`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!"); + `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 endmodule diff --git a/src/stream_xbar.sv b/src/stream_xbar.sv index f2aec305..2b72fad7 100644 --- a/src/stream_xbar.sv +++ b/src/stream_xbar.sv @@ -10,6 +10,8 @@ // Author: Wolfgang Roenninger +`include "common_cells/assertions.svh" + /// Fully connected stream crossbar. /// /// Handshaking rules as defined by the `AMBA AXI` standard on default. @@ -168,46 +170,33 @@ module stream_xbar #( // Assertions // Make sure that the handshake and payload is stable - `ifndef SYNTHESIS `ifndef COMMON_CELLS_ASSERTS_OFF - `ifndef VERILATOR - 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, $sformatf("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, + $sformatf("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, + $sformatf("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, + $sformatf("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, + $sformatf("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, + $sformatf("valid_o at output %0d has been taken away without a ready.", i)) end end - initial begin : proc_parameter_assertions - assert (NumInp > 32'd0) else $fatal(1, "NumInp has to be > 0!"); - assert (NumOut > 32'd0) else $fatal(1, "NumOut has to be > 0!"); - end - `endif + `ASSERT_INIT(numinp_0, NumInp > 32'd0, "NumInp has to be > 0!") + `ASSERT_INIT(numout_0, NumOut > 32'd0, "NumOut has to be > 0!") `endif endmodule