tests/various/shregmap.ys

   1 read_verilog shregmap.v
   2 design -save read
   3
   4 design -copy-to model $__SHREG_DFF_P_
   5 hierarchy -top shregmap_static_test
   6 prep
   7 design -save gold
   8
   9 techmap
  10 shregmap -init
  11
  12 opt
  13
  14 # stat
  15 # show -width
  16 select -assert-count 1 t:$_DFF_P_
  17 select -assert-count 2 t:$__SHREG_DFF_P_
  18
  19 design -stash gate
  20
  21 design -import gold -as gold
  22 design -import gate -as gate
  23 design -copy-from model -as $__SHREG_DFF_P_ \$__SHREG_DFF_P_
  24 prep
  25
  26 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  27 sat -verify -prove-asserts -show-ports -seq 5 miter
  28
  29 #design -load gold
  30 #stat
  31
  32 #design -load gate
  33 #stat