tests/various/dynamic_part_select.ys

   1 ### Original testcase ###
   2 read_verilog ./dynamic_part_select/original.v
   3 proc
   4 rename -top gold
   5 design -stash gold
   6
   7 read_verilog ./dynamic_part_select/original_gate.v
   8 proc
   9 rename -top gate
  10 design -stash gate
  11
  12 design -copy-from gold -as gold gold
  13 design -copy-from gate -as gate gate
  14
  15 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
  16 sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
  17
  18 ### Multiple blocking assingments ###
  19 design -reset
  20 read_verilog ./dynamic_part_select/multiple_blocking.v
  21 proc
  22 rename -top gold
  23 design -stash gold
  24
  25 read_verilog ./dynamic_part_select/multiple_blocking_gate.v
  26 proc
  27 rename -top gate
  28 design -stash gate
  29
  30 design -copy-from gold -as gold gold
  31 design -copy-from gate -as gate gate
  32
  33 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
  34 sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
  35
  36 ### Non-blocking to the same output register ###
  37 design -reset
  38 read_verilog ./dynamic_part_select/nonblocking.v
  39 proc
  40 rename -top gold
  41 design -stash gold
  42
  43 read_verilog ./dynamic_part_select/nonblocking_gate.v
  44 proc
  45 rename -top gate
  46 design -stash gate
  47
  48 design -copy-from gold -as gold gold
  49 design -copy-from gate -as gate gate
  50
  51 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
  52 sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
  53
  54 ### For-loop select, one dynamic input
  55 design -reset
  56 read_verilog ./dynamic_part_select/forloop_select.v
  57 proc
  58 rename -top gold
  59 design -stash gold
  60
  61 read_verilog ./dynamic_part_select/forloop_select_gate.v
  62 proc
  63 rename -top gate
  64 design -stash gate
  65
  66 design -copy-from gold -as gold gold
  67 design -copy-from gate -as gate gate
  68
  69 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
  70 sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
  71
  72 #### Double loop (part-select, reset) ###
  73 design -reset
  74 read_verilog ./dynamic_part_select/reset_test.v
  75 proc
  76 rename -top gold
  77 design -stash gold
  78
  79 read_verilog ./dynamic_part_select/reset_test_gate.v
  80 proc
  81 rename -top gate
  82 design -stash gate
  83
  84 design -copy-from gold -as gold gold
  85 design -copy-from gate -as gate gate
  86
  87 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
  88 sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv
  89
  90 ### Reversed part-select case ###
  91 design -reset
  92 read_verilog ./dynamic_part_select/reversed.v
  93 proc
  94 rename -top gold
  95 design -stash gold
  96
  97 read_verilog ./dynamic_part_select/reversed_gate.v
  98 proc
  99 rename -top gate
 100 design -stash gate
 101
 102 design -copy-from gold -as gold gold
 103 design -copy-from gate -as gate gate
 104
 105 miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
 106 sat -prove-asserts -seq 10 -show-public -verify -set-init-zero equiv