mirror of https://github.com/YosysHQ/yosys.git
81 lines
1.7 KiB
Plaintext
81 lines
1.7 KiB
Plaintext
read_verilog -formal <<EOT
|
|
// From https://github.com/YosysHQ/yosys/pull/4568#issuecomment-2313740948
|
|
|
|
module top(input clk, a, b, c, input [1:0] d, output reg [1:0] q);
|
|
|
|
always @(posedge clk, posedge a, posedge b, posedge c) begin
|
|
if (a) q <= '0;
|
|
else if (b) q <= 2'b10;
|
|
else if (c) q <= '0;
|
|
else q <= d;
|
|
end
|
|
|
|
always @* begin
|
|
if (a) assert(q == '0);
|
|
else if (b) assert(q == 2'b10);
|
|
else if (c) assert(q == '0);
|
|
end
|
|
|
|
endmodule
|
|
EOT
|
|
|
|
proc
|
|
select -assert-count 1 t:$dffsr
|
|
clk2fflogic
|
|
select -assert-count 3 t:$assert
|
|
sat -tempinduct -verify -prove-asserts
|
|
|
|
design -reset
|
|
|
|
read_verilog -formal <<EOT
|
|
// Tests aload combined with reset. The aload gets refactored into the set/reset
|
|
// logic
|
|
module top(input clk, rst, aload_n, input [1:0] l, d, output reg [1:0] q);
|
|
|
|
always @(posedge clk, posedge rst, negedge aload_n) begin
|
|
if (rst) q <= '0;
|
|
else if (!aload_n) q <= l;
|
|
else q <= d;
|
|
end
|
|
|
|
always @* begin
|
|
if (rst) assert(q == '0);
|
|
else if (!aload_n) assert(q == l);
|
|
end
|
|
|
|
endmodule
|
|
EOT
|
|
|
|
proc
|
|
select -assert-count 1 t:$dffsr
|
|
clk2fflogic
|
|
select -assert-count 2 t:$assert
|
|
sat -tempinduct -verify -prove-asserts
|
|
|
|
design -reset
|
|
|
|
read_verilog -formal <<EOT
|
|
// Tests combining of common reset signals
|
|
module top(input clk, rst_a, rst_b, rst_c, input [1:0] d, output reg [1:0] q);
|
|
|
|
always @(posedge clk, posedge rst_a, posedge rst_b, negedge rst_c) begin
|
|
if (rst_a) q <= '1;
|
|
else if (rst_b) q <= '1;
|
|
else if (!rst_c) q <= '1;
|
|
else q <= d;
|
|
end
|
|
|
|
always @* if (rst_a || rst_b || !rst_c) assert(q == '1);
|
|
|
|
endmodule
|
|
|
|
EOT
|
|
|
|
proc
|
|
select -assert-count 1 t:$adff
|
|
clk2fflogic
|
|
select -assert-count 1 t:$assert
|
|
sat -tempinduct -verify -prove-asserts
|
|
|
|
design -reset
|