mirror of
https://github.com/YosysHQ/yosys
synced 2026-04-15 16:54:12 +00:00
20 lines
503 B
Text
20 lines
503 B
Text
read_verilog -noopt <<EOT
|
|
module gold(input i, output o);
|
|
assign o = 1'bx | i;
|
|
endmodule
|
|
EOT
|
|
copy gold coarse
|
|
copy gold fine
|
|
|
|
cd coarse
|
|
opt_expr
|
|
select -assert-none c:* t:$input_port %d
|
|
|
|
cd fine
|
|
opt_expr
|
|
select -assert-none c:* t:$input_port %d
|
|
cd
|
|
miter -equiv -flatten -make_assert -make_outputs coarse fine miter
|
|
sat -verify -prove-asserts -show-ports miter
|
|
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter2
|
|
sat -verify -prove-asserts -show-ports -enable_undef miter2
|