thotypous · February 18, 2025 11:57 · thotypous · Feb 18, 2025
diff --git a/top.sby b/top.sby
 [options]
 mode cover
 depth 20

 [engines]
 smtbmc yices

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

 [files]
 top.v
diff --git a/top.v b/top.v
 module top(input clk);

    reg [31:0] i;
    reg [31:0] j;

    initial begin
        i = 0;
        // if we do not set an initial value for j, the tool will find a value such that the cover statement below is SAT
    end

    always @(posedge clk) begin
        i <= i + 1;
        j <= j + j;
        cover (i == 3 && j == 32);
    end

 endmodule
	module top(input clk);

	reg [31:0] i;
	reg [31:0] j;

	initial begin
	i = 0;
	// if we do not set an initial value for j, the tool will find a value such that the cover statement below is SAT
	end

	always @(posedge clk) begin
	i <= i + 1;
	j <= j + j;
	cover (i == 3 && j == 32);
	end

	endmodule