		Search-engine friendly clone of the ACL2 documentation.

Balance

Balance-core

Signature
(balance-core aignet aignet2 config) → new-aignet2
Arguments: config — Guard (balance-config-p config).

Definitions and Theorems

Function: balance-core

(defun balance-core (aignet aignet2 config)
 (declare (xargs :stobjs (aignet aignet2)))
 (declare (xargs :guard (balance-config-p config)))
 (let ((__function__ 'balance-core))
  (declare (ignorable __function__))
  (b* (((local-stobjs mark copy refcounts levels strash)
        (mv mark
            copy refcounts levels aignet2 strash))
       ((mv copy aignet2)
        (init-copy-comb aignet copy aignet2))
       (refcounts (resize-u32 (num-fanins aignet)
                              refcounts))
       (refcounts (aignet-count-refs refcounts aignet))
       (mark (resize-bits (num-fanins aignet) mark))
       (levels (resize-u32 (+ (num-fanins aignet2)
                              (floor (num-gates aignet) 3))
                           levels))
       ((mv mark copy levels aignet2 strash)
        (aignet-balance-outs 0 config aignet mark
                             copy refcounts levels aignet2 strash))
       ((mv mark copy levels aignet2 strash)
        (aignet-balance-nxsts 0 config aignet mark
                              copy refcounts levels aignet2 strash))
       (aignet2 (finish-copy-comb aignet copy aignet2)))
    (mv mark
        copy refcounts levels aignet2 strash))))

Theorem: num-ins-of-balance-core

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

Theorem: num-regs-of-balance-core

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

Theorem: num-outs-of-balance-core

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

Theorem: balance-core-comb-equivalent

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

Theorem: normalize-input-of-balance-core

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

Theorem: balance-core-of-balance-config-fix-config

(defthm balance-core-of-balance-config-fix-config
  (equal (balance-core aignet
                       aignet2 (balance-config-fix config))
         (balance-core aignet aignet2 config)))

Theorem: balance-core-balance-config-equiv-congruence-on-config

(defthm balance-core-balance-config-equiv-congruence-on-config
  (implies (balance-config-equiv config config-equiv)
           (equal (balance-core aignet aignet2 config)
                  (balance-core aignet aignet2 config-equiv)))
  :rule-classes :congruence)