1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
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
|
