-
Notifications
You must be signed in to change notification settings - Fork 0
/
assertions.svh
201 lines (172 loc) · 9.42 KB
/
assertions.svh
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
191
192
193
194
195
196
197
198
199
200
201
// 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 PRIM_ASSERT_SV
`define PRIM_ASSERT_SV
`ifdef UVM
// report assertion error with UVM if compiled
package assert_rpt_pkg;
import uvm_pkg::*;
`include "uvm_macros.svh"
function void assert_rpt(string msg);
`uvm_error("ASSERT FAILED", msg)
endfunction
endpackage
`endif
///////////////////
// Helper macros //
///////////////////
// local helper macro to reduce code clutter. undefined at the end of this file
`ifndef VERILATOR
`ifndef SYNTHESIS
`ifndef XSIM
`define INC_ASSERT
`endif
`endif
`endif
// Converts an arbitrary block of code into a Verilog string
`define PRIM_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__); \
`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) \
`ifdef INC_ASSERT \
__name: assert (__prop) \
else begin \
`ASSERT_RPT(`PRIM_STRINGIFY(__name)) \
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 \
`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) \
`ifdef INC_ASSERT \
final begin \
__name: assert (__prop || $test$plusargs("disable_assert_final_checks")) \
else begin \
`ASSERT_RPT(`PRIM_STRINGIFY(__name)) \
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 \
`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 \
`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) \
`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) \
`ifdef INC_ASSERT \
`ASSERT(__name, $rose(__sig) |=> !(__sig), __clk, __rst) \
`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) \
`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) \
`ifdef INC_ASSERT \
`ASSERT_KNOWN(__name``KnownEnable, __enable, __clk, __rst) \
`ASSERT_IF(__name, !$isunknown(__sig), __enable, __clk, __rst) \
`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 \
`endif
// Assume an immediate property
`define ASSUME_I(__name, __prop) \
`ifdef INC_ASSERT \
__name: assume (__prop) \
else begin \
`ASSERT_RPT(`PRIM_STRINGIFY(__name)) \
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) \
`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
`endif // PRIM_ASSERT_SV