78 lines
2.3 KiB
Systemverilog
78 lines
2.3 KiB
Systemverilog
|
// DESCRIPTION: Verilator: Verilog Test module
|
||
|
|
//
|
||
|
|
// This file ONLY is placed under the Creative Commons Public Domain.
|
||
|
|
// SPDX-FileCopyrightText: 2026 PlanV GmbH
|
||
|
|
// SPDX-License-Identifier: CC0-1.0
|
||
|
|
|
||
|
|
// verilog_format: off
|
||
|
|
`define stop $stop
|
||
|
|
`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
|
||
|
|
// verilog_format: on
|
||
|
|
|
||
|
|
module t (
|
||
|
|
input clk
|
||
|
|
);
|
||
|
|
|
||
|
|
logic [63:0] crc = 64'h5aef0c8dd70a4497;
|
||
|
|
logic a, b;
|
||
|
|
int cyc = 0;
|
||
|
|
|
||
|
|
int n_imp_no = 0; // cover property (a |=> b) -- non-overlapped implication
|
||
|
|
int n_imp_ov = 0; // cover property (a |-> b) -- overlapped implication
|
||
|
|
int n_seq = 0; // cover property (a ##1 b) -- identity with |=>
|
||
|
|
int n_seq0 = 0; // cover property (a ##0 b) -- identity with |->
|
||
|
|
int n_bool = 0; // cover property (a) -- bare boolean baseline
|
||
|
|
int n_named = 0; // cover property (named pr) -- identity with |=>
|
||
|
|
|
||
|
|
default clocking cb @(posedge clk);
|
||
|
|
endclocking
|
||
|
|
|
||
|
|
assign a = crc[0];
|
||
|
|
assign b = crc[5];
|
||
|
|
|
||
|
|
property pr;
|
||
|
|
a |=> b;
|
||
|
|
endproperty
|
||
|
|
|
||
|
|
cp_imp_no :
|
||
|
|
cover property (a |=> b) n_imp_no++;
|
||
|
|
cp_imp_ov :
|
||
|
|
cover property (a |-> b) n_imp_ov++;
|
||
|
|
cp_seq :
|
||
|
|
cover property (a ##1 b) n_seq++;
|
||
|
|
cp_seq0 :
|
||
|
|
cover property (a ##0 b) n_seq0++;
|
||
|
|
cp_bool :
|
||
|
|
cover property (a) n_bool++;
|
||
|
|
cp_named :
|
||
|
|
cover property (pr) n_named++;
|
||
|
|
|
||
|
|
always @(posedge clk) begin
|
||
|
|
cyc <= cyc + 1;
|
||
|
|
crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[1] ^ crc[0]};
|
||
|
|
if (cyc == 99) begin
|
||
|
|
$write("*-* All Finished *-*\n");
|
||
|
|
$finish;
|
||
|
|
end
|
||
|
|
end
|
||
|
|
|
||
|
|
final begin
|
||
|
|
// A cover of an implication counts only non-vacuous matches (IEEE
|
||
|
|
// 1800-2023 16.15.2): the antecedent must match. So it is identical to the
|
||
|
|
// corresponding sequence cover, not the vacuous implication value.
|
||
|
|
`checkd(n_imp_no, n_seq)
|
||
|
|
`checkd(n_imp_ov, n_seq0)
|
||
|
|
// A named-property cover lowers the same implication, so it also counts
|
||
|
|
// non-vacuously (regression guard for the property-inlining path).
|
||
|
|
`checkd(n_named, n_imp_no)
|
||
|
|
// Pinned Verilator counts; Questa golden cross-checked.
|
||
|
|
`checkd(n_imp_no, 28) // Questa: 28
|
||
|
|
`checkd(n_imp_ov, 27) // Questa: 27
|
||
|
|
`checkd(n_seq, 28) // Questa: 28
|
||
|
|
`checkd(n_seq0, 27) // Questa: 27
|
||
|
|
`checkd(n_bool, 55) // Questa: 54
|
||
|
|
`checkd(n_named, 28) // Questa: 28
|
||
|
|
end
|
||
|
|
|
||
|
|
endmodule
|