mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 19:52:31 +00:00
661fa5ff92
The previous mapping to `$_XOR_` and `$_NOT_` predates the addition of the `$_XNOR_` cell.
139 lines
3.1 KiB
Text
139 lines
3.1 KiB
Text
read_verilog <<EOT
|
|
module top(input a, output [3:0] y);
|
|
assign y[0] = a^1'b0;
|
|
assign y[1] = 1'b1^a;
|
|
assign y[2] = a~^1'b0;
|
|
assign y[3] = 1'b1^~a;
|
|
endmodule
|
|
EOT
|
|
design -save read
|
|
select -assert-count 2 t:$xor
|
|
select -assert-count 2 t:$xnor
|
|
|
|
equiv_opt -assert opt_expr
|
|
design -load postopt
|
|
select -assert-none t:$xor
|
|
select -assert-none t:$xnor
|
|
select -assert-count 2 t:$not
|
|
|
|
|
|
design -load read
|
|
simplemap
|
|
equiv_opt -assert opt_expr
|
|
design -load postopt
|
|
select -assert-none t:$_XOR_
|
|
select -assert-none t:$_XNOR_
|
|
select -assert-count 2 t:$_NOT_
|
|
|
|
design -reset
|
|
read_verilog -icells <<EOT
|
|
module top(input a, output [1:0] y);
|
|
$_XNOR_ u0(.A(a), .B(1'b0), .Y(y[0]));
|
|
$_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1]));
|
|
endmodule
|
|
EOT
|
|
select -assert-count 2 t:$_XNOR_
|
|
equiv_opt -assert opt_expr
|
|
design -load postopt
|
|
select -assert-none t:$_XNOR_
|
|
select -assert-count 1 t:$_NOT_
|
|
|
|
|
|
design -reset
|
|
read_verilog <<EOT
|
|
module top(input a, output [1:0] w, x, y, z);
|
|
assign w = a^1'b0;
|
|
assign x = a^1'b1;
|
|
assign y = a~^1'b0;
|
|
assign z = a~^1'b1;
|
|
endmodule
|
|
EOT
|
|
equiv_opt -assert opt_expr
|
|
|
|
|
|
# Single-bit $xor
|
|
design -reset
|
|
read_verilog -noopt <<EOT
|
|
module gold(input i, output o);
|
|
assign o = 1'bx ^ i;
|
|
endmodule
|
|
EOT
|
|
select -assert-count 1 t:$xor
|
|
copy gold coarse
|
|
copy gold fine
|
|
copy gold coarse_keepdc
|
|
copy gold fine_keepdc
|
|
|
|
cd coarse
|
|
opt_expr
|
|
select -assert-none c:*
|
|
|
|
cd fine
|
|
simplemap
|
|
opt_expr
|
|
select -assert-none c:*
|
|
|
|
cd
|
|
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
|
sat -verify -prove-asserts -show-ports -enable_undef miter
|
|
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
|
|
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
|
|
|
cd coarse_keepdc
|
|
opt_expr -keepdc
|
|
select -assert-count 1 c:*
|
|
|
|
cd fine_keepdc
|
|
simplemap
|
|
opt_expr -keepdc
|
|
select -assert-count 1 c:*
|
|
|
|
cd
|
|
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
|
sat -verify -prove-asserts -show-ports -enable_undef miter3
|
|
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
|
|
sat -verify -prove-asserts -show-ports -enable_undef miter4
|
|
|
|
|
|
# Multi-bit $xor
|
|
design -reset
|
|
read_verilog -noopt <<EOT
|
|
module gold(input i, output [6:0] o);
|
|
assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} ^ {7{i}};
|
|
endmodule
|
|
EOT
|
|
select -assert-count 1 t:$xor
|
|
copy gold coarse
|
|
copy gold fine
|
|
copy gold coarse_keepdc
|
|
copy gold fine_keepdc
|
|
|
|
cd coarse
|
|
opt_expr -fine
|
|
select -assert-count 0 t:$xor
|
|
|
|
cd fine
|
|
simplemap
|
|
opt_expr
|
|
select -assert-none t:$_XOR_
|
|
|
|
cd
|
|
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
|
sat -verify -prove-asserts -show-ports -enable_undef miter
|
|
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
|
|
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
|
|
|
cd coarse_keepdc
|
|
opt_expr -keepdc -fine
|
|
select -assert-count 1 t:$xor
|
|
|
|
cd fine_keepdc
|
|
simplemap
|
|
opt_expr -keepdc
|
|
select -assert-count 3 t:$_XOR_
|
|
|
|
cd
|
|
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
|
sat -verify -prove-asserts -show-ports -enable_undef miter3
|
|
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
|
|
sat -verify -prove-asserts -show-ports -enable_undef miter4
|