mirror of https://github.com/YosysHQ/yosys.git
Added counters sat test case
This commit is contained in:
parent
e915043144
commit
849fd62cfe
|
@ -0,0 +1,35 @@
|
|||
|
||||
module counter1(clk, rst, ping);
|
||||
input clk, rst;
|
||||
output ping;
|
||||
reg [31:0] count;
|
||||
|
||||
always @(posedge clk) begin
|
||||
if (rst)
|
||||
count <= 0;
|
||||
else
|
||||
count <= count + 1;
|
||||
end
|
||||
|
||||
assign ping = &count;
|
||||
endmodule
|
||||
|
||||
module counter2(clk, rst, ping);
|
||||
input clk, rst;
|
||||
output ping;
|
||||
reg [31:0] count;
|
||||
|
||||
integer i;
|
||||
reg carry;
|
||||
|
||||
always @(posedge clk) begin
|
||||
carry = 1;
|
||||
for (i = 0; i < 32; i = i+1) begin
|
||||
count[i] <= !rst & (count[i] ^ carry);
|
||||
carry = count[i] & carry;
|
||||
end
|
||||
end
|
||||
|
||||
assign ping = &count;
|
||||
endmodule
|
||||
|
|
@ -0,0 +1,10 @@
|
|||
|
||||
read_verilog counters.v
|
||||
proc; opt
|
||||
|
||||
expose -shared counter1 counter2
|
||||
miter -equiv -make_assert -make_outputs counter1 counter2 miter
|
||||
|
||||
cd miter; flatten; opt
|
||||
sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs
|
||||
|
Loading…
Reference in New Issue