• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
      • Aignet-copy-init
      • Aignet-simplify-with-tracking
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
      • Aignet-simplify-marked
      • Aignet-complete-copy
      • Aignet-transforms
        • Aignet-output-ranges
        • Aignet-comb-transforms
          • Fraig
          • Parametrize
          • Observability-fix
          • Constprop
          • Apply-m-assumption-n-output-output-transform-default
          • Balance
          • Apply-n-output-comb-transform-default
          • Apply-comb-transform-default
          • Obs-constprop
          • Rewrite
          • Comb-transform
          • Abc-comb-simplify
          • Prune
            • Prune!
          • Rewrite!
          • M-assumption-n-output-comb-transform->name
          • N-output-comb-transform->name
          • Comb-transform->name
          • N-output-comb-transformlist
          • M-assumption-n-output-comb-transformlist
          • Comb-transformlist
          • Apply-comb-transform
        • Aignet-m-assumption-n-output-transforms
        • Aignet-n-output-comb-transforms
      • Aignet-eval
      • Semantics
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Aignet-comb-transforms

Prune

Apply combinational pruning to remove unused nodes in the input network.

Signature

(prune aignet aignet2 config) → new-aignet2

Arguments

aignet — Input aignet.

aignet2 — New aignet -- will be emptied.

config — Settings for the transform.
    Guard (prune-config-p config).

Pruning simply marks the nodes that are in the fanin cones of the combinational outputs and selectively copies only those nodes (but including all combinational inputs). This transform is usually redundant because most transforms result in pruned networks. One use is to restore xor nodes after applying the abc-comb-simplify transform, since the aiger format used for translating between ABC and aignet does not support xors.

Definitions and Theorems

Function: prune

(defun prune (aignet aignet2 config)
  (declare (xargs :stobjs (aignet aignet2)))
  (declare (xargs :guard (prune-config-p config)))
  (let ((__function__ 'prune))
    (declare (ignorable __function__))
    (aignet-prune-comb aignet aignet2
                       (prune-config->gatesimp config))))

Theorem: num-ins-of-prune

(defthm num-ins-of-prune
  (b* ((?new-aignet2 (prune aignet aignet2 config)))
    (equal (stype-count :pi new-aignet2)
           (stype-count :pi aignet))))

Theorem: num-regs-of-prune

(defthm num-regs-of-prune
  (b* ((?new-aignet2 (prune aignet aignet2 config)))
    (equal (stype-count :reg new-aignet2)
           (stype-count :reg aignet))))

Theorem: num-outs-of-prune

(defthm num-outs-of-prune
  (b* ((?new-aignet2 (prune aignet aignet2 config)))
    (equal (stype-count :po new-aignet2)
           (stype-count :po aignet))))

Theorem: prune-comb-equivalent

(defthm prune-comb-equivalent
  (b* ((?new-aignet2 (prune aignet aignet2 config)))
    (comb-equiv new-aignet2 aignet)))

Theorem: normalize-input-of-prune

(defthm normalize-input-of-prune
  (implies (syntaxp (not (equal aignet2 ''nil)))
           (equal (prune aignet aignet2 config)
                  (prune aignet nil config))))

Subtopics

Prune!

Like prune, but overwrites the original network instead of returning a new one.