mirror of https://github.com/YosysHQ/yosys.git
33 lines
478 B
Plaintext
33 lines
478 B
Plaintext
|
read_verilog <<EOT
|
||
|
|
module gold(
|
||
|
|
input wire [7:0] a,
|
||
|
|
input wire [7:0] b,
|
||
|
|
output wire [7:0] c
|
||
|
|
);
|
||
|
|
|
||
|
|
wire [7:0] b_neg;
|
||
|
|
assign b_neg = -b;
|
||
|
|
assign c = a + b_neg;
|
||
|
|
endmodule
|
||
|
|
|
||
|
|
module gate(
|
||
|
|
input wire [7:0] a,
|
||
|
|
input wire [7:0] b,
|
||
|
|
output wire [7:0] c
|
||
|
|
);
|
||
|
|
|
||
|
|
wire [7:0] b_neg;
|
||
|
|
assign b_neg = ~b + 1;
|
||
|
|
assign c = a + b_neg;
|
||
|
|
endmodule
|
||
|
|
|
||
|
|
EOT
|
||
|
|
|
||
|
|
equiv_make -make_assert gold gate miter
|
||
|
|
|
||
|
|
select -assert-count 0 t:$equiv
|
||
|
|
select -assert-count 2 t:$assert
|
||
|
|
|
||
|
|
prep -top miter
|
||
|
|
sat -prove-asserts -verify
|