-
Notifications
You must be signed in to change notification settings - Fork 752
/
prim_assert.sv
190 lines (168 loc) · 9.73 KB
/
prim_assert.sv
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
// Copyright lowRISC contributors (OpenTitan project).
// 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 PRIM_ASSERT_SV
`define PRIM_ASSERT_SV
///////////////////
// Helper macros //
///////////////////
// Default clk and reset signals used by assertion macros below.
`define ASSERT_DEFAULT_CLK clk_i
`define ASSERT_DEFAULT_RST !rst_ni
// Converts an arbitrary block of code into a Verilog string
`define PRIM_STRINGIFY(__x) `"__x`"
// ASSERT_ERROR logs an error message with either `uvm_error or with $error.
//
// This somewhat duplicates `DV_ERROR macro defined in hw/dv/sv/dv_utils/dv_macros.svh. The reason
// for redefining it here is to avoid creating a dependency.
`define ASSERT_ERROR(__name) \
`ifdef UVM \
uvm_pkg::uvm_report_error("ASSERT FAILED", `PRIM_STRINGIFY(__name), uvm_pkg::UVM_NONE, \
`__FILE__, `__LINE__, "", 1); \
`else \
$error("%0t: (%0s:%0d) [%m] [ASSERT FAILED] %0s", $time, `__FILE__, `__LINE__, \
`PRIM_STRINGIFY(__name)); \
`endif
// This macro is suitable for conditionally triggering lint errors, e.g., if a Sec parameter takes
// on a non-default value. This may be required for pre-silicon/FPGA evaluation but we don't want
// to allow this for tapeout.
`define ASSERT_STATIC_LINT_ERROR(__name, __prop) \
localparam int __name = (__prop) ? 1 : 2; \
always_comb begin \
logic unused_assert_static_lint_error; \
unused_assert_static_lint_error = __name'(1'b1); \
end
// Static assertions for checks inside SV packages. If the conditions is not true, this will
// trigger an error during elaboration.
`define ASSERT_STATIC_IN_PACKAGE(__name, __prop) \
function automatic bit assert_static_in_package_``__name(); \
bit unused_bit [((__prop) ? 1 : -1)]; \
unused_bit = '{default: 1'b0}; \
return unused_bit[0]; \
endfunction
// The basic helper macros are actually defined in "implementation headers". The macros should do
// the same thing in each case (except for the dummy flavour), but in a way that the respective
// tools support.
//
// If the tool supports assertions in some form, we also define INC_ASSERT (which can be used to
// hide signal definitions that are only used for assertions).
//
// The list of basic macros supported is:
//
// ASSERT_I: Immediate assertion. Note that immediate assertions are sensitive to simulation
// glitches.
//
// ASSERT_INIT: Assertion in initial block. Can be used for things like parameter checking.
//
// ASSERT_INIT_NET: Assertion in initial block. Can be used for initial value of a net.
//
// ASSERT_FINAL: 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.
//
// ASSERT_AT_RESET: Assertion just before reset. Can be used to check sum-like properties that get
// cleared at reset.
// Note that unless your simulation ends with a reset, the property does not get
// checked at end of simulation; use ASSERT_AT_RESET_AND_FINAL if the property
// should also get checked at end of simulation.
//
// ASSERT_AT_RESET_AND_FINAL: Assertion just before reset and in final block. Can be used to check
// sum-like properties before every reset and at the end of simulation.
//
// ASSERT: Assert a concurrent property directly. It can be called as a module (or
// interface) body item.
//
// Note: 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_NEVER: Assert a concurrent property NEVER happens
//
// ASSERT_KNOWN: 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.
//
// COVER: Cover a concurrent property
//
// ASSUME: Assume a concurrent property
//
// ASSUME_I: Assume an immediate property
`ifdef VERILATOR
`include "prim_assert_dummy_macros.svh"
`elsif SYNTHESIS
`include "prim_assert_dummy_macros.svh"
`elsif YOSYS
`include "prim_assert_yosys_macros.svh"
`define INC_ASSERT
`else
`include "prim_assert_standard_macros.svh"
`define INC_ASSERT
`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) \
`ASSERT(__name, $rose(__sig) |=> !(__sig), __clk, __rst)
// 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) \
`ASSERT(__name, (__enable) |-> (__prop), __clk, __rst)
// 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) \
`ifndef FPV_ON \
`ASSERT_KNOWN(__name``KnownEnable, __enable, __clk, __rst) \
`ASSERT_IF(__name, !$isunknown(__sig), __enable, __clk, __rst) \
`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) \
`ifdef FPV_ON \
`ASSUME(__name, __prop, __clk, __rst) \
`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) \
`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
// FPV assertion that proves that the FSM control flow is linear (no loops)
// The sequence triggers whenever the state changes and stores the current state as "initial_state".
// Then thereafter we must never see that state again until reset.
// It is possible for the reset to release ahead of the clock.
// Create a small "gray" window beyond the usual rst time to avoid
// checking.
`define ASSERT_FPV_LINEAR_FSM(__name, __state, __type, __clk = `ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST) \
`ifdef INC_ASSERT \
bit __name``_cond; \
always_ff @(posedge __clk or posedge __rst) begin \
if (__rst) begin \
__name``_cond <= 0; \
end else begin \
__name``_cond <= 1; \
end \
end \
property __name``_p; \
__type initial_state; \
(!$stable(__state) & __name``_cond, initial_state = $past(__state)) |-> \
(__state != initial_state) until (__rst == 1'b1); \
endproperty \
`ASSERT(__name, __name``_p, __clk, 0) \
`endif
`include "prim_assert_sec_cm.svh"
`include "prim_flop_macros.sv"
`endif // PRIM_ASSERT_SV