1 read_verilog pmux2shiftx.v
4 hierarchy -top pmux2shiftx_test
8 pmux2shiftx -min_density 70
14 select -assert-count 1 t:$sub
15 select -assert-count 1 t:$mux
16 select -assert-count 1 t:$shift
17 select -assert-count 3 t:$shiftx
21 design -import gold -as gold
22 design -import gate -as gate
24 miter -equiv -flatten -make_assert -make_outputs gold gate miter
25 sat -verify -prove-asserts -show-ports miter
34 hierarchy -top issue01135
38 select -assert-count 0 t:$shift*
39 select -assert-count 1 t:$pmux