tests/various/abc9.ys

   1 read_verilog abc9.v
   2 design -save read
   3 hierarchy -top abc9_test027
   4 proc
   5 design -save gold
   6
   7 abc9 -lut 4
   8 check
   9 design -stash gate
  10
  11 design -import gold -as gold
  12 design -import gate -as gate
  13
  14 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  15 sat -verify -prove-asserts -show-ports miter
  16
  17
  18 design -load read
  19 hierarchy -top abc9_test028
  20 proc
  21
  22 abc9 -lut 4
  23 select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i
  24 select -assert-count 1 t:unknown
  25 select -assert-none t:$lut t:unknown %% t: %D
  26
  27
  28 design -load read
  29 hierarchy -top abc9_test032
  30 proc
  31 clk2fflogic
  32 design -save gold
  33
  34 abc9 -lut 4
  35 check
  36 design -stash gate
  37
  38 design -import gold -as gold
  39 design -import gate -as gate
  40
  41 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  42 sat -seq 10 -verify -prove-asserts -show-ports miter
  43
  44
  45 design -reset
  46 read_verilog -icells <<EOT
  47 module abc9_test036(input clk, d, output q);
  48 (* keep, init=1'b0 *) wire w;
  49 $_DFF_P_ ff(.C(clk), .D(d), .Q(w));
  50 assign q = w;
  51 endmodule
  52 EOT
  53 equiv_opt -assert abc9 -lut 4 -dff
  54 design -load postopt
  55 cd abc9_test036
  56 select -assert-count 1 t:$_DFF_P_
  57 select -assert-none t:* t:$_DFF_P_ %d
  58
  59
  60 design -reset
  61 read_verilog -icells -specify <<EOT
  62 (* abc9_lut=1, blackbox *)
  63 module LUT2(input [1:0] i, output o);
  64 parameter [3:0] mask = 0;
  65 assign o = i[0] ? (i[1] ? mask[3] : mask[2])
  66                 : (i[1] ? mask[1] : mask[0]);
  67 specify
  68   (i *> o) = 1;
  69 endspecify
  70 endmodule
  71
  72 module abc9_test037(input [1:0] i, output o);
  73 LUT2 #(.mask(4'b0)) lut (.i(i), .o(o));
  74 endmodule
  75 EOT
  76 abc9
  77
  78
  79 design -reset
  80 read_verilog -icells <<EOT
  81 module abc9_test038(input clk, output w, x, y, z);
  82 (* init=1'b1 *) wire w;
  83 $_DFF_N_ ff1(.C(clk), .D(1'b1), .Q(w));
  84 (* init=1'bx *) wire x;
  85 $_DFF_N_ ff2(.C(clk), .D(1'b0), .Q(x));
  86 (* init=1'b0 *) wire y;
  87 $_DFF_N_ ff3(.C(clk), .D(1'b0), .Q(y));
  88 (* init=1'b0 *) wire z;
  89 $_DFF_N_ ff4(.C(clk), .D(1'b1), .Q(z));
  90 endmodule
  91 EOT
  92 simplemap
  93 equiv_opt -assert abc9 -lut 4 -dff
  94 design -load postopt
  95 cd abc9_test038
  96 select -assert-count 3 t:$_DFF_N_
  97 select -assert-none c:ff1 c:ff2 c:ff4 %% c:* %D
  98 clean
  99 select -assert-count 2 a:init
 100 select -assert-count 1 w:w a:init %i
 101 select -assert-count 1 c:ff4 %co c:ff4 %d %a a:init %i
 102
 103
 104 # Check that non-dangling ABC9 black-boxes are preserved
 105 design -reset
 106 read_verilog -specify <<EOT
 107 (* abc9_box, blackbox *)
 108 module mux_with_param(input I0, I1, S, output O);
 109 parameter P = 0;
 110 specify
 111     (I0 => O) = P;
 112     (I1 => O) = P;
 113     (S => O) = P;
 114 endspecify
 115 endmodule
 116
 117 module abc9_test039(output O);
 118   mux_with_param #(.P(1)) m (
 119     .I0(1'b1),
 120     .I1(1'b1),
 121     .O(O),
 122     .S(1'b0)
 123   );
 124 endmodule
 125 EOT
 126 abc9 -lut 4
 127 cd abc9_test039
 128 select -assert-count 1 t:mux_with_param
 129
 130
 131 # Check that dangling ABC9 black-boxes are swept away
 132 design -reset
 133 read_verilog -specify <<EOT
 134 (* abc9_box, blackbox *)
 135 module mux_with_param(input I0, I1, S, output O);
 136 parameter P = 0;
 137 specify
 138     (I0 => O) = P;
 139     (I1 => O) = P;
 140     (S => O) = P;
 141 endspecify
 142 endmodule
 143
 144 module abc9_test040(output O);
 145   wire w;
 146   mux_with_param #(.P(1)) m (
 147     .I0(1'b1),
 148     .I1(1'b1),
 149     .O(w),
 150     .S(1'b0)
 151   );
 152 endmodule
 153 EOT
 154 abc9 -lut 4
 155 cd abc9_test040
 156 select -assert-count 0 t:mux_with_param