forked from github/verilator
118 lines
2.9 KiB
Coq
118 lines
2.9 KiB
Coq
|
// DESCRIPTION: Verilator: Verilog Test module
|
||
|
//
|
||
|
// This file ONLY is placed into the Public Domain, for any use,
|
||
|
// without warranty, 2007 by Wilson Snyder.
|
||
|
|
||
|
module t (/*AUTOARG*/
|
||
|
// Inputs
|
||
|
clk
|
||
|
);
|
||
|
|
||
|
input clk;
|
||
|
reg toggle;
|
||
|
integer cyc; initial cyc=1;
|
||
|
|
||
|
Test test (/*AUTOINST*/
|
||
|
// Inputs
|
||
|
.clk (clk),
|
||
|
.toggle (toggle),
|
||
|
.cyc (cyc[31:0]));
|
||
|
|
||
|
always @ (posedge clk) begin
|
||
|
if (cyc!=0) begin
|
||
|
cyc <= cyc + 1;
|
||
|
toggle <= !cyc[0];
|
||
|
if (cyc==9) begin
|
||
|
end
|
||
|
if (cyc==10) begin
|
||
|
$write("*-* All Finished *-*\n");
|
||
|
$finish;
|
||
|
end
|
||
|
end
|
||
|
end
|
||
|
|
||
|
endmodule
|
||
|
|
||
|
module Test
|
||
|
(
|
||
|
input clk,
|
||
|
input toggle,
|
||
|
input [31:0] cyc
|
||
|
);
|
||
|
|
||
|
// Simple cover
|
||
|
cover property (@(posedge clk) cyc==3);
|
||
|
|
||
|
// With statement, in generate
|
||
|
generate if (1) begin
|
||
|
cover property (@(posedge clk) cyc==4) $display("*COVER: Cyc==4");
|
||
|
end
|
||
|
endgenerate
|
||
|
|
||
|
// Labeled cover
|
||
|
cyc_eq_5:
|
||
|
cover property (@(posedge clk) cyc==5) $display("*COVER: Cyc==5");
|
||
|
|
||
|
// Using default clock
|
||
|
default clocking @(posedge clk);
|
||
|
cover property (cyc==6) $display("*COVER: Cyc==6");
|
||
|
endclocking
|
||
|
|
||
|
// Disable statement
|
||
|
// Note () after disable are required
|
||
|
cover property (@(posedge clk) disable iff (toggle) cyc==8)
|
||
|
$display("*COVER: Cyc==8");
|
||
|
cover property (@(posedge clk) disable iff (!toggle) cyc==8)
|
||
|
$stop;
|
||
|
|
||
|
`ifndef verilator // Unsupported
|
||
|
// Using a more complicated property
|
||
|
property C1;
|
||
|
@(posedge clk)
|
||
|
disable iff (!toggle)
|
||
|
cyc==5;
|
||
|
endproperty
|
||
|
cover property (C1) $display("*COVER: Cyc==5");
|
||
|
|
||
|
// Using covergroup
|
||
|
// Note a covergroup is really inheritance of a special system "covergroup" class.
|
||
|
covergroup counter1 @ (posedge cyc);
|
||
|
// Automatic methods: stop(), start(), sample(), set_inst_name()
|
||
|
|
||
|
// Each bin value must be <= 32 bits. Strange.
|
||
|
cyc_value : coverpoint cyc {
|
||
|
}
|
||
|
|
||
|
cyc_bined : coverpoint cyc {
|
||
|
bins zero = {0};
|
||
|
bins low = {1,5};
|
||
|
// Note 5 is also in the bin above. Only the first bin matching is counted.
|
||
|
bins mid = {[5:$]};
|
||
|
// illegal_bins // Has precidence over "first matching bin", creates assertion
|
||
|
// ignore_bins // Not counted, and not part of total
|
||
|
}
|
||
|
toggle : coverpoint (toggle) {
|
||
|
bins off = {0};
|
||
|
bins on = {1};
|
||
|
}
|
||
|
cyc5 : coverpoint (cyc==5) {
|
||
|
bins five = {1};
|
||
|
}
|
||
|
|
||
|
// option.at_least = {number}; // Default 1 - Hits to be considered covered
|
||
|
// option.auto_bin_max = {number}; // Default 64
|
||
|
// option.comment = {string}
|
||
|
// option.goal = {number}; // Default 90%
|
||
|
// option.name = {string}
|
||
|
// option.per_instance = 1; // Default 0 - each instance separately counted (cadence default is 1)
|
||
|
// option.weight = {number}; // Default 1
|
||
|
|
||
|
// CROSS
|
||
|
value_and_toggle: // else default is __<firstlabel>_X_<secondlabel>_<n>
|
||
|
cross cyc_value, toggle;
|
||
|
endgroup
|
||
|
counter1 c1 = new();
|
||
|
`endif
|
||
|
|
||
|
endmodule
|