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
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
|
/* Generated by vpassert; File:"verilog/example.v" */
`line 1 "verilog/example.v" 0
// DESCRIPTION: Example top verilog file for vpassert program
// This file ONLY is placed into the Public Domain, for any use,
// without warranty, 2000-2012 by Wilson Snyder.
`timescale 1ns/1ns
module example;/*vpassert*/integer __message; initial __message = 5;reg _assertreqack1_busy_r; initial _assertreqack1_busy_r = 0;reg _assertreqack1_data0_r; initial _assertreqack1_data0_r = 0;reg _ucoverclk10; initial _ucoverclk10 = 0;reg _ucoverclk11; initial _ucoverclk11 = 0;reg _ucoverclk12; initial _ucoverclk12 = 0;reg _ucoverclk13; initial _ucoverclk13 = 0;reg _ucoverclk14; initial _ucoverclk14 = 0;reg _ucoverclk15; initial _ucoverclk15 = 0;reg _ucoverclk16; initial _ucoverclk16 = 0;reg _ucoverclk17; initial _ucoverclk17 = 0;
reg _ucoverclk18; initial _ucoverclk18 = 0;reg _ucoverclk19; initial _ucoverclk19 = 0;reg _ucoverclk20; initial _ucoverclk20 = 0;reg _ucoverclk21; initial _ucoverclk21 = 0;reg _ucoverclk22; initial _ucoverclk22 = 0;reg _ucoverclk23; initial _ucoverclk23 = 0;reg _ucoverclk24; initial _ucoverclk24 = 0;reg _ucoverclk25; initial _ucoverclk25 = 0;reg _ucoverclk26; initial _ucoverclk26 = 0;reg _ucoverclk27; initial _ucoverclk27 = 0;reg _ucoverclk28; initial _ucoverclk28 = 0;
reg _ucoverclk29; initial _ucoverclk29 = 0;reg _ucoverclk3; initial _ucoverclk3 = 0;reg _ucoverclk30; initial _ucoverclk30 = 0;reg _ucoverclk4; initial _ucoverclk4 = 0;reg _ucoverclk5; initial _ucoverclk5 = 0;reg _ucoverclk6; initial _ucoverclk6 = 0;reg _ucoverclk7; initial _ucoverclk7 = 0;reg _ucoverclk8; initial _ucoverclk8 = 0;reg _ucoverclk9; initial _ucoverclk9 = 0;reg _umessageclk2; initial _umessageclk2 = 0;
`line 7 "verilog/example.v" 0
pli pli (); // Put on highest level of your design
integer i;
`define ten 10
reg \escaped[10] ;
initial begin
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/begin $callInfo ("Welcome to a VPASSERTed file\n"); end end /*vpassert*/
/*VCS coverage on*/
`line 18 "verilog/example.v" 0
//
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if ((__message >= (1))) begin $callInfo ("Printed only at debug level %0d\n", 1); end end /*vpassert*/
/*VCS coverage on*/
`line 20 "verilog/example.v" 0
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if ((__message >= (9))) begin $callInfo ("Printed only at debug level %0d\n", 9); end end /*vpassert*/
/*VCS coverage on*/
`line 21 "verilog/example.v" 0
//
\escaped[10] = 1'b1;
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (!(\escaped[10] ) && (`__message_on)) begin $callError ("Escaped not 1\n%%E: In %m\n"); end end /*vpassert*/
/*VCS coverage on*/
`line 24 "verilog/example.v" 0
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (!(\escaped[10] ) && (`__message_on)) begin $callInfo ("Escaped not 1\n"); end end /*vpassert*/
/*VCS coverage on*/
`line 25 "verilog/example.v" 0
//
i=0;
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (!(1==1) && (`__message_on)) begin $callError ("Why doesn't 1==1??\n%%E: In %m\n"); end end /*vpassert*/
/*VCS coverage on*/
`line 28 "verilog/example.v" 0
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (!(10==`ten) && (`__message_on)) begin $callError ("Why doesn't 10==10??\n%%E: In %m\n"); end end /*vpassert*/
/*VCS coverage on*/
`line 36 "verilog/example.v" 0
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (!(1==1) && (`__message_on)) begin $callError ("Why doesn't 1==1??\n%%E: In %m\n"); end end /*vpassert*/
/*VCS coverage on*/
`line 36 "verilog/example.v" 0
//
i=3'b100; if ((({i [2:0]}) & (({i [2:0]}) - 3'b1)) !== 3'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("MULTIPLE ACTIVE %b --> amone ok\n\n%%E: In %m\n", ({i [2:0]})); end end /*vpassert*/
/*VCS coverage on*/
`line 38 "verilog/example.v" 0
i=3'b010; if ((({i[2:0]}) & (({i[2:0]}) - 3'b1)) !== 3'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("MULTIPLE ACTIVE %b --> amone ok\n\n%%E: In %m\n", ({i[2:0]})); end end /*vpassert*/
/*VCS coverage on*/
`line 39 "verilog/example.v" 0
i=3'b001; if ((({i[2:0]}) & (({i[2:0]}) - 3'b1)) !== 3'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("MULTIPLE ACTIVE %b --> amone ok\n\n%%E: In %m\n", ({i[2:0]})); end end /*vpassert*/
/*VCS coverage on*/
`line 40 "verilog/example.v" 0
i=3'b000; if ((({i[2:0]}) & (({i[2:0]}) - 3'b1)) !== 3'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("MULTIPLE ACTIVE %b --> amone ok\n\n%%E: In %m\n", ({i[2:0]})); end end /*vpassert*/
/*VCS coverage on*/
`line 41 "verilog/example.v" 0
//i=3'b011; $uassert_amone(i[2:0], "amone error expected\n");
//i=3'b110; $uassert_amone(i[2:0], "amone error expected\n");
//
i=2'b10; if ((({i[1:0]}) & (({i[1:0]}) - 2'b1)) !== 2'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("MULTIPLE ACTIVE %b --> onehot ok\n\n%%E: In %m\n", ({i[1:0]})); end end /*vpassert*/
/*VCS coverage on*/
`line 45 "verilog/example.v" 0
if (({i[1:0]}) === 2'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("NONE ACTIVE %b --> onehot ok\n\n%%E: In %m\n", ({i[1:0]})); end end /*vpassert*/
/*VCS coverage on*/
`line 45 "verilog/example.v" 0
i=2'b01; if ((({i[1:0]}) & (({i[1:0]}) - 2'b1)) !== 2'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("MULTIPLE ACTIVE %b --> onehot ok\n\n%%E: In %m\n", ({i[1:0]})); end end /*vpassert*/
/*VCS coverage on*/
`line 46 "verilog/example.v" 0
if (({i[1:0]}) === 2'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("NONE ACTIVE %b --> onehot ok\n\n%%E: In %m\n", ({i[1:0]})); end end /*vpassert*/
/*VCS coverage on*/
`line 46 "verilog/example.v" 0
i=2'b10; if ((({i[1],i[0]}) & (({i[1],i[0]}) - 2'b1)) !== 2'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("MULTIPLE ACTIVE %b --> onehot ok\n\n%%E: In %m\n", ({i[1],i[0]})); end end /*vpassert*/
/*VCS coverage on*/
`line 47 "verilog/example.v" 0
if (({i[1],i[0]}) === 2'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("NONE ACTIVE %b --> onehot ok\n\n%%E: In %m\n", ({i[1],i[0]})); end end /*vpassert*/
/*VCS coverage on*/
`line 47 "verilog/example.v" 0
i=2'b10; if ((({{i[1],i[0]}}) & (({{i[1],i[0]}}) - 2'b1)) !== 2'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("MULTIPLE ACTIVE %b --> onehot ok\n\n%%E: In %m\n", ({{i[1],i[0]}})); end end /*vpassert*/
/*VCS coverage on*/
`line 48 "verilog/example.v" 0
if (({{i[1],i[0]}}) === 2'b0 && `__message_on)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("NONE ACTIVE %b --> onehot ok\n\n%%E: In %m\n", ({{i[1],i[0]}})); end end /*vpassert*/
/*VCS coverage on*/
`line 48 "verilog/example.v" 0
//i=2'b11; $uassert_onehot(i[2:0], "onehot error expected\n");
//i=2'b00; $uassert_onehot(i[2:0], "onehot error expected\n");
end
// Test assertions within case statements
initial begin
i=3'b100;
casez (i)
3'b100: ;
3'b000: $stop;
3'b010:
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("Why?\n%%E: In %m\n"); end end /*vpassert*/
/*VCS coverage on*/
`line 59 "verilog/example.v" 0
default: $stop;
endcase
if ($time > 1000) $stop;
end
// Example of request/grant handshake
reg clk;
reg bus_req; // Request a transaction, single cycle pulse
reg bus_ack; // Acknowledged transaction, single cycle pulse
reg [31:0] bus_data;
initial begin
// Reset signals
bus_req = 1'b0;
bus_ack = 1'b0;
bus_data = 1'b0;
// Assert a request
@ (posedge clk) ;
bus_req = 1'b1;
bus_data = 32'hfeed;
// Wait for ack
@ (posedge clk) ;
bus_req = 1'b0;
// Send ack
@ (posedge clk) ;
bus_ack = 1'b1;
// Next request could be here
@ (posedge clk) ;
bus_ack = 1'b0;
end
always @ (posedge clk) begin
`line 93 "verilog/example.v" 0
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/
`line 93 "verilog/example.v" 0
if (`__message_on) begin casez({(_assertreqack1_busy_r),(bus_req),(bus_ack)}) 3'b000: ; 3'b010: _assertreqack1_busy_r<=1'b1; 3'b011: begin if (`__message_on) begin $callError ("Unexpected bus_req coincident with bus_ack\n%%E: In %m\n"); end end 3'b001: begin if (`__message_on) begin $callError ("Unexpected bus_ack with no request pending\n%%E: In %m\n"); end end 3'b100: ; 3'b11?: begin if (`__message_on) begin $callError ("Unexpected bus_req with request already pending\n%%E: In %m\n"); end end 3'b101: _assertreqack1_busy_r<=1'b0;endcase if ((bus_req)||(_assertreqack1_busy_r)) begin if ((_assertreqack1_busy_r)) begin if (_assertreqack1_data0_r != ^(bus_data)) begin if (`__message_on) begin $callError ("Unexpected transition of bus_data during transaction\n%%E: In %m\n"); end end end _assertreqack1_data0_r <= ^(bus_data); end end end /*vpassert*/
/*VCS coverage on*/
`line 93 "verilog/example.v" 0
end
// Overall control loop
initial clk = 1'b0;
initial forever begin
#1;
i = i + 1;
clk = !clk;
if (i==20)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callWarn ("Don't know what to do next!\n%%W: In %m\n"); end end /*vpassert*/
/*VCS coverage on*/
`line 102 "verilog/example.v" 0
if (i==22)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callError ("Guess I'll error out!\n%%E: In %m\n"); end end /*vpassert*/
/*VCS coverage on*/
`line 103 "verilog/example.v" 0
end
// Moved clock asserts
always @* begin/*vpassert*/ _ucoverclk30=1'b0; /*vpassert*//*vpassert*/ _ucoverclk29=1'b0; /*vpassert*//*vpassert*/ _ucoverclk28=1'b0; /*vpassert*//*vpassert*/ _ucoverclk27=1'b0; /*vpassert*//*vpassert*/ _ucoverclk26=1'b0; /*vpassert*//*vpassert*/ _ucoverclk25=1'b0; /*vpassert*//*vpassert*/ _ucoverclk24=1'b0; /*vpassert*//*vpassert*/ _ucoverclk23=1'b0; /*vpassert*//*vpassert*/ _ucoverclk22=1'b0; /*vpassert*//*vpassert*/ _ucoverclk21=1'b0; /*vpassert*//*vpassert*/ _ucoverclk20=1'b0; /*vpassert*//*vpassert*/ _ucoverclk19=1'b0; /*vpassert*//*vpassert*/ _ucoverclk18=1'b0; /*vpassert*//*vpassert*/ _ucoverclk17=1'b0; /*vpassert*//*vpassert*/ _ucoverclk16=1'b0; /*vpassert*//*vpassert*/ _ucoverclk15=1'b0; /*vpassert*//*vpassert*/ _ucoverclk14=1'b0; /*vpassert*//*vpassert*/ _ucoverclk13=1'b0; /*vpassert*//*vpassert*/ _ucoverclk12=1'b0; /*vpassert*//*vpassert*/ _ucoverclk11=1'b0; /*vpassert*//*vpassert*/ _ucoverclk10=1'b0; /*vpassert*//*vpassert*/ _ucoverclk9=1'b0; /*vpassert*//*vpassert*/ _ucoverclk8=1'b0; /*vpassert*//*vpassert*/ _ucoverclk7=1'b0; /*vpassert*//*vpassert*/ _ucoverclk6=1'b0; /*vpassert*//*vpassert*/ _ucoverclk5=1'b0; /*vpassert*//*vpassert*/ _ucoverclk4=1'b0; /*vpassert*//*vpassert*/ _ucoverclk3=1'b0; /*vpassert*//*vpassert*/ _umessageclk2=1'b0; /*vpassert*/
if (i==19) /*vpassert*/_umessageclk2=1'b1;/*vpassert*/
if (i==18) /*vpassert*/_ucoverclk3=1'b1;/*vpassert*/
/*vpassert*/_ucoverclk4=( (i[(27)]));/*vpassert*//*vpassert*/_ucoverclk5=( (i[(26)]));/*vpassert*//*vpassert*/_ucoverclk6=( (i[(25)]));/*vpassert*//*vpassert*/_ucoverclk7=( (i[(24)]));/*vpassert*//*vpassert*/_ucoverclk8=( (i[(23)]));/*vpassert*//*vpassert*/_ucoverclk9=( (i[(22)]));/*vpassert*//*vpassert*/_ucoverclk10=( (i[(21)]));/*vpassert*//*vpassert*/_ucoverclk11=( (i[(20)]));/*vpassert*//*vpassert*/_ucoverclk12=( (i[(19)]));/*vpassert*//*vpassert*/_ucoverclk13=( (i[(18)]));/*vpassert*//*vpassert*/_ucoverclk14=( (i[(17)]));/*vpassert*//*vpassert*/_ucoverclk15=( (i[(16)]));/*vpassert*//*vpassert*/_ucoverclk16=( (i[(15)]));/*vpassert*//*vpassert*/_ucoverclk17=( (i[(14)]));/*vpassert*//*vpassert*/_ucoverclk18=( (i[(13)]));/*vpassert*//*vpassert*/_ucoverclk19=( (i[(12)]));/*vpassert*//*vpassert*/_ucoverclk20=( (i[(11)]));/*vpassert*//*vpassert*/_ucoverclk21=( (i[(10)]));/*vpassert*//*vpassert*/_ucoverclk22=( (i[(9)]));/*vpassert*//*vpassert*/_ucoverclk23=( (i[(8)]));/*vpassert*//*vpassert*/_ucoverclk24=( (i[(7)]));/*vpassert*//*vpassert*/_ucoverclk25=( (i[(6)]));/*vpassert*//*vpassert*/_ucoverclk26=( (i[(5)]));/*vpassert*//*vpassert*/_ucoverclk27=( (i[(4)]));/*vpassert*//*vpassert*/_ucoverclk28=( (i[(3)]));/*vpassert*//*vpassert*/_ucoverclk29=( (i[(1)]));/*vpassert*//*vpassert*/_ucoverclk30=( (i[(0)]));/*vpassert*/
end
// Meta coverage disables
initial begin
// vp_coverage_off
`line 114 "verilog/example.v" 0
/*VCS coverage off*/
/*verilator coverage_off*/
/*vpassert*/
`line 115 "verilog/example.v" 0
if (0) begin end // cover off'ed
// vp_coverage_on
`line 116 "verilog/example.v" 0
/*vpassert*/
/*verilator coverage_on*/
/*VCS coverage on*/
`line 117 "verilog/example.v" 0
end
// Ifdef based disables
initial begin
`ifndef NEVER
`ifdef SYNTHESIS
if (1) begin end // cover on
`elsif SYNTHESIS
if (1) begin end // cover on
`else
if (1) begin end // cover off'ed
`endif
`ifndef SYNTHESIS
if (1) begin end // cover off'ed
`else
if (1) begin end // cover on
`endif
`endif
end
`line 135 "verilog/example.v" 0
always @ (posedge clk) if (_umessageclk2)
/*VCS coverage off*/
/*vpassert*/begin /*verilator coverage_block_off*/if (`__message_on) begin $callWarn ("Called at next edge (1 of 2)\n%%W: In %m\n"); end end /*vpassert*/
/*VCS coverage on*/
`line 109 "verilog/example.v" 0
example_cover_label: cover property (@(posedge clk) (_ucoverclk3));
foreach_label__27: cover property (@(posedge clk) (_ucoverclk4));
`line 110 "verilog/example.v" 0
foreach_label__26: cover property (@(posedge clk) (_ucoverclk5));
`line 110 "verilog/example.v" 0
foreach_label__25: cover property (@(posedge clk) (_ucoverclk6));
`line 110 "verilog/example.v" 0
foreach_label__24: cover property (@(posedge clk) (_ucoverclk7));
`line 110 "verilog/example.v" 0
foreach_label__23: cover property (@(posedge clk) (_ucoverclk8));
`line 110 "verilog/example.v" 0
foreach_label__22: cover property (@(posedge clk) (_ucoverclk9));
`line 110 "verilog/example.v" 0
foreach_label__21: cover property (@(posedge clk) (_ucoverclk10));
`line 110 "verilog/example.v" 0
foreach_label__20: cover property (@(posedge clk) (_ucoverclk11));
`line 110 "verilog/example.v" 0
foreach_label__19: cover property (@(posedge clk) (_ucoverclk12));
`line 110 "verilog/example.v" 0
foreach_label__18: cover property (@(posedge clk) (_ucoverclk13));
`line 110 "verilog/example.v" 0
foreach_label__17: cover property (@(posedge clk) (_ucoverclk14));
`line 110 "verilog/example.v" 0
foreach_label__16: cover property (@(posedge clk) (_ucoverclk15));
`line 110 "verilog/example.v" 0
foreach_label__15: cover property (@(posedge clk) (_ucoverclk16));
`line 110 "verilog/example.v" 0
foreach_label__14: cover property (@(posedge clk) (_ucoverclk17));
`line 110 "verilog/example.v" 0
foreach_label__13: cover property (@(posedge clk) (_ucoverclk18));
`line 110 "verilog/example.v" 0
foreach_label__12: cover property (@(posedge clk) (_ucoverclk19));
`line 110 "verilog/example.v" 0
foreach_label__11: cover property (@(posedge clk) (_ucoverclk20));
`line 110 "verilog/example.v" 0
foreach_label__10: cover property (@(posedge clk) (_ucoverclk21));
`line 110 "verilog/example.v" 0
foreach_label__9: cover property (@(posedge clk) (_ucoverclk22));
`line 110 "verilog/example.v" 0
foreach_label__8: cover property (@(posedge clk) (_ucoverclk23));
`line 110 "verilog/example.v" 0
foreach_label__7: cover property (@(posedge clk) (_ucoverclk24));
`line 110 "verilog/example.v" 0
foreach_label__6: cover property (@(posedge clk) (_ucoverclk25));
`line 110 "verilog/example.v" 0
foreach_label__5: cover property (@(posedge clk) (_ucoverclk26));
`line 110 "verilog/example.v" 0
foreach_label__4: cover property (@(posedge clk) (_ucoverclk27));
`line 110 "verilog/example.v" 0
foreach_label__3: cover property (@(posedge clk) (_ucoverclk28));
`line 110 "verilog/example.v" 0
foreach_label__1: cover property (@(posedge clk) (_ucoverclk29));
`line 110 "verilog/example.v" 0
foreach_label__0: cover property (@(posedge clk) (_ucoverclk30));
`line 136 "verilog/example.v" 0
endmodule
`line 139 "verilog/example.v" 0
|
