Struct SimpleAigOpt

pub struct SimpleAigOpt;

Implements simple AIG optimizations.

The following transformations are done:

• multi-bit And, Or, Xor, Not are bitblasted
• single-bit And, Or are transformed into Aig
• Not cells on Aig inputs are merged into the Aig
• Not cells on Xor inputs are pushed onto the output
• const folding:
  • ~0 -> 1
  • ~1 -> 0
  • ~X -> X
  • a & 0 -> 0
  • a & 1 -> a
  • a ^ 0 -> a
  • a ^ 1 -> ~a
  • a ^ X -> X
• idempotence:
  • a & a -> a
  • (a & b) & a -> a
  • (a & b) & (a & c) -> (a & b) & c
• contradiction:
  • a & ~a -> 0
  • (a & b) & ~a -> 0
  • (a & b) & (~a & c) -> 0
• subsumption:
  • (a | b) & a -> a
  • (a | b) & (a & c) -> a & c
• resolution:
  • (a | b) & (~a | b) -> b
• substitution:
  • (a | b) & ~b -> a & ~b
  • (a | b) & (~b & c) -> a & (~b & c)
  • (a ^ b) & ~b -> a & ~b
  • (a ^ b) & b -> ~a & b
  • ~(a ^ b) & ~b -> ~a & ~b
  • ~(a ^ b) & b -> a & b
  • (a ^ b) & (~b & c) -> a & (~b & c)
  • (a ^ b) & (b & c) -> ~a & (b & c)
  • ~(a ^ b) & (~b & c) -> ~a & (~b & c)
  • ~(a ^ b) & (b & c) -> a & (b & c)
• XOR folding:
  • a ^ a -> 0
  • (a ^ b) ^ a -> b
  • (a ^ b) ^ (a ^ c) -> b ^ c
• AND-XOR optimization:
  • (a & b) ^ a -> a & ~b
  • (a & b) ^ ~a -> ~(a & ~b)
• XOR recognition:
  • ~(a & b) & ~(~a & ~b) -> a ^ b

All rules above are replicated for any commutation of operands, and any negation of inputs.

This ruleset ensures that any fragment of the netlist including only Not, And, Or, Xor, Aig cells will be transformed into a fragment containing only Aig, single-bit Xor, and single-bit Not cells, with the single-bit Not cells only present when required by non-Aig non-Xor cell inputs.

The optimizations performed here are mostly borrowed from https://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf and have an important property described in the paper: they will never create more than one new cell (Not cells don’t count), and they will not increase the logic level. Thus, they can never make the netlist “worse”.

Trait Implementations

impl RewriteRuleset for SimpleAigOpt

fn rewrite<'a>( &self, cell: &Cell, meta: MetaItemRef<'a>, _output: Option<&Value>, rewriter: &Rewriter<'a>, ) -> RewriteResult<'a>

fn cell_added(&self, design: &Design, cell: &Cell, output: &Value)

fn net_replaced(&self, design: &Design, from: Net, to: Net)