prjunnamed_generic/rewrite/aig.rs
1use prjunnamed_netlist::{
2 Cell, ControlNet, MetaItemRef, Net, RewriteNetSource, RewriteResult, RewriteRuleset, Rewriter, Value,
3};
4
5/// Implements simple AIG optimizations.
6///
7/// The following transformations are done:
8///
9/// - multi-bit And, Or, Xor, Not are bitblasted
10/// - single-bit And, Or are transformed into Aig
11/// - Not cells on Aig inputs are merged into the Aig
12/// - Not cells on Xor inputs are pushed onto the output
13/// - const folding:
14/// - ~0 -> 1
15/// - ~1 -> 0
16/// - ~X -> X
17/// - a & 0 -> 0
18/// - a & 1 -> a
19/// - a ^ 0 -> a
20/// - a ^ 1 -> ~a
21/// - a ^ X -> X
22/// - idempotence:
23/// - a & a -> a
24/// - (a & b) & a -> a
25/// - (a & b) & (a & c) -> (a & b) & c
26/// - contradiction:
27/// - a & ~a -> 0
28/// - (a & b) & ~a -> 0
29/// - (a & b) & (~a & c) -> 0
30/// - subsumption:
31/// - (a | b) & a -> a
32/// - (a | b) & (a & c) -> a & c
33/// - resolution:
34/// - (a | b) & (~a | b) -> b
35/// - substitution:
36/// - (a | b) & ~b -> a & ~b
37/// - (a | b) & (~b & c) -> a & (~b & c)
38/// - (a ^ b) & ~b -> a & ~b
39/// - (a ^ b) & b -> ~a & b
40/// - ~(a ^ b) & ~b -> ~a & ~b
41/// - ~(a ^ b) & b -> a & b
42/// - (a ^ b) & (~b & c) -> a & (~b & c)
43/// - (a ^ b) & (b & c) -> ~a & (b & c)
44/// - ~(a ^ b) & (~b & c) -> ~a & (~b & c)
45/// - ~(a ^ b) & (b & c) -> a & (b & c)
46/// - XOR folding:
47/// - a ^ a -> 0
48/// - (a ^ b) ^ a -> b
49/// - (a ^ b) ^ (a ^ c) -> b ^ c
50/// - AND-XOR optimization:
51/// - (a & b) ^ a -> a & ~b
52/// - (a & b) ^ ~a -> ~(a & ~b)
53/// - XOR recognition:
54/// - ~(a & b) & ~(~a & ~b) -> a ^ b
55///
56/// All rules above are replicated for any commutation of operands, and any negation of inputs.
57///
58/// This ruleset ensures that any fragment of the netlist including only Not, And, Or, Xor, Aig cells will
59/// be transformed into a fragment containing only Aig, single-bit Xor, and single-bit Not cells, with the single-bit
60/// Not cells only present when required by non-Aig non-Xor cell inputs.
61///
62/// The optimizations performed here are mostly borrowed from <https://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf>
63/// and have an important property described in the paper: they will never create more than one new cell (Not cells
64/// don't count), and they will not increase the logic level. Thus, they can never make the netlist "worse".
65pub struct SimpleAigOpt;
66
67impl RewriteRuleset for SimpleAigOpt {
68 fn rewrite<'a>(
69 &self,
70 cell: &Cell,
71 meta: MetaItemRef<'a>,
72 _output: Option<&Value>,
73 rewriter: &Rewriter<'a>,
74 ) -> RewriteResult<'a> {
75 match *cell {
76 Cell::Not(ref val) if val.len() == 1 => {
77 let net = val[0];
78 if net == Net::ZERO {
79 return Net::ONE.into();
80 }
81 if net == Net::ONE {
82 return Net::ZERO.into();
83 }
84 if net == Net::UNDEF {
85 return Net::UNDEF.into();
86 }
87 let src = rewriter.find_cell(net);
88 if let RewriteNetSource::Cell(cell, _, bit) = src
89 && let Cell::Not(ref val) = *cell
90 {
91 return val[bit].into();
92 }
93 RewriteResult::None
94 }
95
96 Cell::Aig(net1, net2) => {
97 for (net_a, net_b) in [(net1, net2), (net2, net1)] {
98 let src_a = rewriter.find_cell(net_a.net());
99 let src_b = rewriter.find_cell(net_b.net());
100
101 // idempotence: a & a -> a
102 if net_a == net_b {
103 return net_a.into();
104 }
105
106 // contradiction: a & ~a, a & 0 -> 0
107 if net_a == !net_b || net_b.is_always(false) {
108 return Net::ZERO.into();
109 }
110
111 // identity: a & 1 -> a
112 if net_b.is_always(true) {
113 return net_a.into();
114 }
115
116 // merge inverters into AIG cell
117 if let RewriteNetSource::Cell(ref cell_a, meta_a, bit) = src_a
118 && let Cell::Not(ref val) = **cell_a
119 {
120 let new_a = ControlNet::from_net_invert(val[bit], !net_a.is_negative());
121 return RewriteResult::CellMeta(Cell::Aig(new_a, net_b), meta.merge(meta_a));
122 }
123
124 if let RewriteNetSource::Cell(ref cell_a, _, _) = src_a
125 && let Cell::Aig(net_a1, net_a2) = **cell_a
126 && net_a.is_positive()
127 {
128 // (aa & ab) & b
129 for (net_aa, _net_ab) in [(net_a1, net_a2), (net_a2, net_a1)] {
130 // idempotence: (aa & ab) & aa -> aa & ab
131 if net_aa == net_b {
132 return net_a.into();
133 }
134 // contradiction: (aa & ab) & ~aa -> 0
135 if net_aa == !net_b {
136 return Net::ZERO.into();
137 }
138
139 if let RewriteNetSource::Cell(ref cell_b, _, _) = src_b
140 && let Cell::Aig(net_b1, net_b2) = **cell_b
141 && net_b.is_positive()
142 {
143 // (aa & ab) & (ba & bb)
144 for (net_ba, net_bb) in [(net_b1, net_b2), (net_b2, net_b1)] {
145 // idempotence: (aa & ab) & (aa & bb) -> (aa & ab) & bb
146 if net_aa == net_ba {
147 return Cell::Aig(net_a, net_bb).into();
148 }
149 // contradiction: (aa & ab) & (~aa & bb) -> 0
150 if net_aa == !net_ba {
151 return Net::ZERO.into();
152 }
153 }
154 }
155 }
156 }
157
158 if let RewriteNetSource::Cell(ref cell_a, meta_a, _) = src_a
159 && let Cell::Aig(net_a1, net_a2) = **cell_a
160 && net_a.is_negative()
161 {
162 // ~(aa & ab) & b
163 for (net_aa, net_ab) in [(net_a1, net_a2), (net_a2, net_a1)] {
164 // substitution: ~(aa & ab) & aa -> ~ab & aa
165 if net_aa == net_b {
166 return Cell::Aig(!net_ab, net_b).into();
167 }
168 // subsumption: ~(aa & ab) & ~aa -> ~aa
169 if net_aa == !net_b {
170 return net_b.into();
171 }
172
173 if let RewriteNetSource::Cell(ref cell_b, _, _) = src_b
174 && let Cell::Aig(net_b1, net_b2) = **cell_b
175 && net_b.is_positive()
176 {
177 // ~(aa & ab) & (ba & bb)
178 for (net_ba, _net_bb) in [(net_b1, net_b2), (net_b2, net_b1)] {
179 // substitution: ~(aa & ab) & (aa & bb) -> ~ab & (aa & bb)
180 if net_aa == net_ba {
181 return Cell::Aig(!net_ab, net_b).into();
182 }
183 // subsumption: ~(aa & ab) & (~aa & bb) -> (~aa & bb)
184 if net_aa == !net_ba {
185 return net_b.into();
186 }
187 }
188 }
189
190 if let RewriteNetSource::Cell(ref cell_b, meta_b, _) = src_b
191 && let Cell::Aig(net_b1, net_b2) = **cell_b
192 && net_b.is_negative()
193 {
194 // ~(aa & ab) & ~(ba & bb)
195 for (net_ba, net_bb) in [(net_b1, net_b2), (net_b2, net_b1)] {
196 // resolution: ~(aa & ab) & ~(~aa & ab) -> ~ab
197 if net_aa == !net_ba && net_ab == net_bb {
198 return (!net_ab).into();
199 }
200 // XOR recognition: ~(aa & ab) & ~(~aa & ~ab) -> aa ^ ab
201 if net_aa == !net_ba && net_ab == !net_bb {
202 let xor_meta = meta.merge(meta_a).merge(meta_b);
203 let xor = Cell::Xor(net_aa.net().into(), net_ab.net().into());
204 if net_aa.is_negative() ^ net_ab.is_negative() {
205 let xor = rewriter.add_cell_meta(xor, xor_meta);
206 return Cell::Not(xor).into();
207 } else {
208 return RewriteResult::CellMeta(xor.into(), xor_meta);
209 }
210 }
211 }
212 }
213 }
214 }
215
216 if let RewriteNetSource::Cell(ref cell_a, _, bit) = src_a
217 && let Cell::Xor(ref val_a1, ref val_a2) = **cell_a
218 {
219 let inv_a = net_a.is_negative();
220 let net_a1 = val_a1[bit];
221 let net_a2 = val_a2[bit];
222 // (aa ^ ab) & b
223 for (net_aa, net_ab) in [(net_a1, net_a2), (net_a2, net_a1)] {
224 // substitution: (aa ^ ab) & aa -> ~ab & aa
225 // substitution: ~(aa ^ ab) & aa -> ab & aa
226 // substitution: (aa ^ ab) & ~aa -> ab & ~aa
227 // substitution: ~(aa ^ ab) & ~aa -> ~ab & ~aa
228 if net_aa == net_b.net() {
229 let inv = !(inv_a ^ net_b.is_negative());
230 return Cell::Aig(ControlNet::from_net_invert(net_ab, inv), net_b).into();
231 }
232
233 if let RewriteNetSource::Cell(ref cell_b, _, _) = src_b
234 && let Cell::Aig(net_b1, net_b2) = **cell_b
235 && net_b.is_positive()
236 {
237 // (aa ^ ab) & (ba & bb)
238 for (net_ba, _net_bb) in [(net_b1, net_b2), (net_b2, net_b1)] {
239 // substitution: (aa ^ ab) & (aa & bb) -> ~ab & aa
240 // substitution: ~(aa ^ ab) & (aa & bb) -> ab & aa
241 // substitution: (aa ^ ab) & (~aa & bb) -> ab & ~aa
242 // substitution: ~(aa ^ ab) & (~aa & bb) -> ~ab & ~aa
243 if net_aa == net_ba.net() {
244 let inv = !(inv_a ^ net_ba.is_negative());
245 return Cell::Aig(ControlNet::from_net_invert(net_ab, inv), net_b).into();
246 }
247 }
248 }
249 }
250 }
251 }
252
253 RewriteResult::None
254 }
255
256 Cell::Xor(ref val1, ref val2) if val1.len() == 1 => {
257 let net1 = val1[0];
258 let net2 = val2[0];
259 for (net_a, net_b) in [(net1, net2), (net2, net1)] {
260 let src_a = rewriter.find_cell(net_a);
261 let src_b = rewriter.find_cell(net_b);
262
263 // a ^ a -> 0
264 if net_a == net_b {
265 return Net::ZERO.into();
266 }
267
268 // a ^ X -> X
269 if net_b == Net::UNDEF {
270 return Net::UNDEF.into();
271 }
272
273 // a ^ 0 -> a
274 if net_b == Net::ZERO {
275 return net_a.into();
276 }
277
278 // a ^ 1 -> ~a
279 if net_b == Net::ONE {
280 return Cell::Not(net_a.into()).into();
281 }
282
283 // !a ^ b -> !(a ^ b)
284 if let RewriteNetSource::Cell(ref cell_a, meta_a, bit) = src_a
285 && let Cell::Not(ref val) = **cell_a
286 {
287 let meta = meta.merge(meta_a);
288 let xor = rewriter.add_cell_meta(Cell::Xor(val[bit].into(), net_b.into()), meta);
289 return RewriteResult::CellMeta(Cell::Not(xor), meta);
290 }
291
292 if let RewriteNetSource::Cell(ref cell_a, meta_a, _) = src_a
293 && let Cell::Aig(net_a1, net_a2) = **cell_a
294 {
295 // (aa & ab) ^ b
296 for (net_aa, net_ab) in [(net_a1, net_a2), (net_a2, net_a1)] {
297 // (aa & ab) ^ aa -> aa & ~ab
298 let meta = meta.merge(meta_a);
299 if net_aa == ControlNet::Pos(net_b) {
300 return RewriteResult::CellMeta(Cell::Aig(net_aa, !net_ab), meta);
301 }
302 // (aa & ab) ^ ~aa -> ~(aa & ~ab)
303 if net_aa == ControlNet::Neg(net_b) {
304 let aig = rewriter.add_cell(Cell::Aig(net_aa, !net_ab));
305 return RewriteResult::CellMeta(Cell::Not(aig), meta);
306 }
307 }
308 }
309
310 if let RewriteNetSource::Cell(ref cell_a, meta_a, bit) = src_a
311 && let Cell::Xor(ref val_a1, ref val_a2) = **cell_a
312 {
313 let net_a1 = val_a1[bit];
314 let net_a2 = val_a2[bit];
315 // (aa ^ ab) ^ b
316 for (net_aa, net_ab) in [(net_a1, net_a2), (net_a2, net_a1)] {
317 // (aa ^ ab) ^ aa -> ab
318 if net_aa == net_b {
319 return net_ab.into();
320 }
321
322 if let RewriteNetSource::Cell(ref cell_b, meta_b, bit) = src_b
323 && let Cell::Xor(ref val_b1, ref val_b2) = **cell_b
324 {
325 let net_b1 = val_b1[bit];
326 let net_b2 = val_b2[bit];
327 // (aa ^ ab) ^ (ba ^ bb)
328 for (net_ba, net_bb) in [(net_b1, net_b2), (net_b2, net_b1)] {
329 // (aa ^ ab) ^ (aa ^ bb) -> ab ^ bb
330 if net_aa == net_ba {
331 let meta = meta.merge(meta_a).merge(meta_b);
332 return RewriteResult::CellMeta(
333 Cell::Xor(net_ab.into(), net_bb.into()).into(),
334 meta,
335 );
336 }
337 }
338 }
339 }
340 }
341 }
342 RewriteResult::None
343 }
344
345 // Split bitwise Not and Xor into single-bit cells.
346 Cell::Not(ref val) => {
347 let mut result = Value::new();
348 for net in val {
349 result.extend(rewriter.add_cell(Cell::Not(net.into())));
350 }
351 result.into()
352 }
353 Cell::Xor(ref val_a, ref val_b) => {
354 let mut result = Value::new();
355 for (net_a, net_b) in val_a.iter().zip(val_b.iter()) {
356 result.extend(rewriter.add_cell(Cell::Xor(net_a.into(), net_b.into())));
357 }
358 result.into()
359 }
360
361 // Convert And and Or into AIG.
362 Cell::And(ref val_a, ref val_b) => {
363 let mut result = Value::new();
364 for (net_a, net_b) in val_a.iter().zip(val_b.iter()) {
365 result.extend(rewriter.add_cell(Cell::Aig(net_a.into(), net_b.into())));
366 }
367 result.into()
368 }
369 Cell::Or(ref val_a, ref val_b) => {
370 let mut result = Value::new();
371 for (net_a, net_b) in val_a.iter().zip(val_b.iter()) {
372 let aig = rewriter.add_cell(Cell::Aig(ControlNet::Neg(net_a), ControlNet::Neg(net_b)));
373 result.extend(rewriter.add_cell(Cell::Not(aig)));
374 }
375 result.into()
376 }
377
378 _ => RewriteResult::None,
379 }
380 }
381}