walker.sby

[tasks]
cvr

[options]
cvr: mode cover
multiclock on
depth 360

[engines]
smtbmc

[script]
read -formal walker.v
prep -top walker

[files]
walker.v

walker.v

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