read_verilog splice.v
hierarchy -check; opt
copy test gold

cd test
splice
# show

cd ..
rename test gate
miter -equiv -make_assert -make_outputs gold gate miter

flatten miter
sat -verify -prove-asserts -show-inputs -show-outputs miter