| read_verilog pmux2shiftx.v |
| design -save read |
| |
| hierarchy -top pmux2shiftx_test |
| prep |
| design -save gold |
| |
| pmux2shiftx -min_density 70 |
| |
| opt |
| |
| stat |
| # show -width |
| select -assert-count 1 t:$sub |
| select -assert-count 1 t:$mux |
| select -assert-count 1 t:$shift |
| select -assert-count 3 t:$shiftx |
| |
| design -stash gate |
| |
| design -import gold -as gold |
| design -import gate -as gate |
| |
| miter -equiv -flatten -make_assert -make_outputs gold gate miter |
| sat -verify -prove-asserts -show-ports miter |
| |
| #design -load gold |
| #stat |
| # |
| #design -load gate |
| #stat |
| |
| design -load read |
| hierarchy -top issue01135 |
| proc |
| pmux2shiftx -norange |
| opt -full |
| select -assert-count 0 t:$shift* |
| select -assert-count 1 t:$pmux |
