Created
December 23, 2019 14:05
-
-
Save ZipCPU/bf70b248341942c00afd4ed42bdad165 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
[tasks] | |
cvr | |
[options] | |
cvr: mode cover | |
multiclock on | |
depth 360 | |
[engines] | |
smtbmc | |
[script] | |
read -formal walker.v | |
prep -top walker | |
[files] | |
walker.v |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module walker(i_clk,o_led); | |
input i_clk; | |
output reg [7:0] o_led; | |
reg clk; | |
reg [31:0]count; | |
reg reverse; | |
// parameter CLK_RATE_HZ = 100000000; | |
parameter CLK_RATE_HZ = 2; | |
initial begin | |
o_led = 8'b0000_0001; | |
clk = 0; | |
count = 0; | |
reverse = 0; | |
end | |
// generating clk of 1hz | |
always_ff @(posedge i_clk) begin | |
if(count < CLK_RATE_HZ/2 ) count<=count+1; | |
else begin | |
clk<=~clk; | |
count<=0; | |
end | |
end | |
// turn on the next led after 1s using 1hz clk | |
always @(posedge clk) begin | |
if (o_led == 128) reverse = 1; | |
else if (o_led == 1) reverse = 0; | |
if(reverse) o_led = o_led>>1; | |
else o_led = o_led<<1; | |
end | |
`ifdef FORMAL | |
reg f_past_valid; | |
reg [3:0] cvr_counter; | |
(* gclk *) reg gbl_clk; | |
initial f_past_valid = 0; | |
always @(posedge i_clk) | |
f_past_valid <= 1; | |
always @(posedge gbl_clk) | |
assume(i_clk == !$past(i_clk)); | |
initial cvr_counter = 0; | |
always @(posedge i_clk) | |
if (f_past_valid && $rose(clk) && o_led == 1) | |
cvr_counter <= cvr_counter + 1; | |
always @(*) | |
cover(cvr_counter > 2); | |
`endif | |
endmodule |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment