Loading files
This file is pinned to the selected release. Download the original to open it in your design tool.
// Copyright lowRISC contributors.
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
// SPDX-License-Identifier: Apache-2.0
// Macros and helper code for using assertions.
// - Provides default clk and rst options to simplify code
// - Provides boiler plate template for common assertions
`ifndef COMMON_CELLS_ASSERTIONS_SVH
`define COMMON_CELLS_ASSERTIONS_SVH
///////////////////
// Helper macros //
///////////////////
// helper macro to reduce code clutter, can be used to hide signal defs only used for assertions
`ifndef ASSERTS_OFF
`ifndef SYNTHESIS
`ifndef XILINX_SIMULATOR
`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
// detect and resolve potential collision with lowRISC's prim_assert macros by undefining all of
// their macros (the variants in here should be backwards compatible with lowRISC's macros)
`ifdef PRIM_ASSERT_SV
`ifdef INC_ASSERT
`undef ASSERT_I
`undef ASSERT_INIT
`undef ASSERT_FINAL
`undef ASSERT
`undef ASSERT_NEVER
`undef ASSERT_KNOWN
`undef COVER
`undef ASSERT_PULSE
`undef ASSERT_IF
`ifndef FPV_ON
`undef ASSERT_KNOWN_IF
`endif
`undef ASSUME
`undef ASSUME_I
`endif
`ifdef FPV_ON
`undef ASSUME_FPV
`undef ASSUME_I_FPV
`undef COVER_FPV
`endif
`endif
// define PRIM_ASSERT_SV to anticipate a later inclusion of lowRISC's prim_assert macros
`define PRIM_ASSERT_SV
// Converts an arbitrary block of code into a Verilog string
`define ASSERT_STRINGIFY(__x) `"__x`"
// ASSERT_RPT is available to change the reporting mechanism when an assert fails
`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
///////////////////////////////////////
// Simple assertion and cover macros //
///////////////////////////////////////
// Default clk and reset signals used by assertion macros below.
`define ASSERT_DEFAULT_CLK clk_i
`define ASSERT_DEFAULT_RST !rst_ni
// Immediate assertion
// Note that immediate assertions are sensitive to simulation glitches.
`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, __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, __desc = "") \
`ifdef INC_ASSERT \
final begin \
__name: assert (__prop || $test$plusargs("disable_assert_final_checks")) \
else begin \
`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, __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, __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, __desc = "") \
`ifdef INC_ASSERT \
`ASSERT(__name, !$isunknown(__sig), __clk, __rst, __desc) \
`endif
// Cover a concurrent property
`define COVER(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \
`ifdef INC_ASSERT \
__name: cover property (@(posedge __clk) disable iff ((__rst) !== '0) (__prop)); \
`endif
//////////////////////////////
// Complex assertion macros //
//////////////////////////////
// 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, __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, __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, __desc = "") \
`ifdef INC_ASSERT \
`ASSERT_KNOWN(__name``KnownEnable, __enable, __clk, __rst, __desc) \
`ASSERT_IF(__name, !$isunknown(__sig), __enable, __clk, __rst, __desc) \
`endif
// Assert that (unmasked parts of) data are stable when valid is high and ready is low.
`define ASSERT_STABLE(__name, __valid, __ready, __data, __mask = '0, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST, __desc = "") \
`ifdef INC_ASSERT \
`ASSERT(__name, (__valid) && !(__ready) |=> $stable((__data) & ~(__mask)), __clk, __rst, __desc) \
`endif
///////////////////////
// Assumption macros //
///////////////////////
// Assume a concurrent property
`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, __desc = "") \
`ifdef INC_ASSERT \
__name: assume (__prop) \
else begin \
`ASSERT_RPT(`ASSERT_STRINGIFY(__name), __desc) \
end \
`endif
//////////////////////////////////
// For formal verification only //
//////////////////////////////////
// Note that the existing set of ASSERT macros specified above shall be used for FPV,
// thereby ensuring that the assertions are evaluated during DV simulations as well.
// ASSUME_FPV
// Assume a concurrent property during formal verification only.
`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, __desc = "") \
`ifdef FPV_ON \
`ASSUME_I(__name, __prop, __desc) \
`endif
// COVER_FPV
// Cover a concurrent property during formal verification
`define COVER_FPV(__name, __prop, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \
`ifdef FPV_ON \
`COVER(__name, __prop, __clk, __rst) \
`endif
`endif // COMMON_CELLS_ASSERTIONS_SVH
e73baaec2This file is pinned to the selected release. Download the original to open it in your design tool.