mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-05 09:04:08 +00:00
fbf5d89587
This adds a -make_assert flag to equiv_make. When used, the pass generates $eqx and $assert cells to encode equivalence instead of $equiv.
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
|