|
|
|---|
|
|
|
|---|
Apply combinational SAT sweeping (fraiging) to remove redundancies in the input network.
(fraig strict-count aignet aignet2 config output-ranges state) → (mv new-aignet2 new-output-ranges new-state)
Note: This fraiging implementation is heavily based on the one in ABC, developed and maintained at Berkeley by Alan Mishchenko.
Settings for the transform can be tweaked using the
When used as a n-output-comb-transform or m-assumption-n-output-comb-transform (i.e. when we don't need to keep strict
combinational equivalence), the FRAIG transform can track, as an
(aignet::make-fraig-config ... ;; Save the remaining equivalences resulting from this transform :save-candidate-equivs-as :fraig-remaining-equiv-classes ;; Do a final simulation if there are any pending counterexamples at the end of the SAT sweep, ;; to ensure we've broken all the equivalence classes we've gotten counterexamples for: :final-force-resim t ...) (aignet::make-fraig-config ... ;; Read the recorded candidate equivalences as our starting equivalence classes :output-types `((:fraig-remaining-equiv-classes . ,(aignet::fraig-output-type-initial-equiv-classes))) ...)
Configured this way, the subsequent FRAIG transform doesn't need to
re-disprove candidate equivalences that are difficult to contradict through
random simulation; if the previous FRAIG transform already found a
counterexample to the equivalence and that equivalence was then resimulated,
then it will no longer be present in the equivalence classes. The resimulation
can be forced by setting the
Function:
(defun fraig (strict-count aignet aignet2 config output-ranges state) (declare (xargs :stobjs (aignet aignet2 state))) (declare (xargs :guard (and (acl2::maybe-natp strict-count) (fraig-config-p config) (aignet-output-range-map-p output-ranges)))) (declare (xargs :guard (or (not strict-count) (<= strict-count (num-outs aignet))))) (let ((__function__ 'fraig)) (declare (ignorable __function__)) (b* (((local-stobjs aignet-tmp) (mv aignet2 aignet-tmp output-ranges state)) ((mv aignet-tmp output-ranges state) (fraig-core strict-count aignet aignet-tmp config output-ranges state)) (aignet2 (aignet-prune-comb aignet-tmp aignet2 (fraig-config->gatesimp config)))) (mv aignet2 aignet-tmp output-ranges state))))
Theorem:
(defthm aignet-output-range-map-p-of-fraig.new-output-ranges (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig strict-count aignet aignet2 config output-ranges state))) (aignet-output-range-map-p new-output-ranges)) :rule-classes :rewrite)
Theorem:
(defthm num-ins-of-fraig (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig strict-count aignet aignet2 config output-ranges state))) (equal (stype-count :pi new-aignet2) (stype-count :pi aignet))))
Theorem:
(defthm num-regs-of-fraig (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig strict-count aignet aignet2 config output-ranges state))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet))))
Theorem:
(defthm output-ranges-length-of-fraig (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig strict-count aignet aignet2 config output-ranges state))) (equal (aignet-output-range-map-length new-output-ranges) (stype-count :po new-aignet2))))
Theorem:
(defthm num-outs-of-fraig (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig strict-count aignet aignet2 config output-ranges state))) (implies (not strict-count) (equal (stype-count :po new-aignet2) (stype-count :po aignet)))))
Theorem:
(defthm num-outs-lower-bound-of-fraig-nonstrict (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig strict-count aignet aignet2 config output-ranges state))) (implies strict-count (<= (nfix strict-count) (stype-count :po new-aignet2)))) :rule-classes :linear)
Theorem:
(defthm fraig-comb-equivalent (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig strict-count aignet aignet2 config output-ranges state))) (implies (not strict-count) (comb-equiv new-aignet2 aignet))))
Theorem:
(defthm output-eval-of-fraig-when-nonstrict (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig strict-count aignet aignet2 config output-ranges state))) (implies (and strict-count (< (nfix i) (nfix strict-count))) (equal (output-eval i invals regvals new-aignet2) (output-eval i invals regvals aignet)))))
Theorem:
(defthm normalize-input-of-fraig (implies (syntaxp (not (equal aignet2 ''nil))) (equal (fraig strict-count aignet aignet2 config output-ranges state) (fraig strict-count aignet nil config output-ranges state))))
Theorem:
(defthm w-state-of-fraig (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig strict-count aignet aignet2 config output-ranges state))) (equal (w new-state) (w state))))
Theorem:
(defthm fraig-of-maybe-natp-fix-strict-count (equal (fraig (acl2::maybe-natp-fix strict-count) aignet aignet2 config output-ranges state) (fraig strict-count aignet aignet2 config output-ranges state)))
Theorem:
(defthm fraig-maybe-nat-equiv-congruence-on-strict-count (implies (acl2::maybe-nat-equiv strict-count strict-count-equiv) (equal (fraig strict-count aignet aignet2 config output-ranges state) (fraig strict-count-equiv aignet aignet2 config output-ranges state))) :rule-classes :congruence)
Theorem:
(defthm fraig-of-fraig-config-fix-config (equal (fraig strict-count aignet aignet2 (fraig-config-fix config) output-ranges state) (fraig strict-count aignet aignet2 config output-ranges state)))
Theorem:
(defthm fraig-fraig-config-equiv-congruence-on-config (implies (fraig-config-equiv config config-equiv) (equal (fraig strict-count aignet aignet2 config output-ranges state) (fraig strict-count aignet aignet2 config-equiv output-ranges state))) :rule-classes :congruence)
Theorem:
(defthm fraig-of-aignet-output-range-map-fix-output-ranges (equal (fraig strict-count aignet aignet2 config (aignet-output-range-map-fix output-ranges) state) (fraig strict-count aignet aignet2 config output-ranges state)))
Theorem:
(defthm fraig-aignet-output-range-map-equiv-congruence-on-output-ranges (implies (aignet-output-range-map-equiv output-ranges output-ranges-equiv) (equal (fraig strict-count aignet aignet2 config output-ranges state) (fraig strict-count aignet aignet2 config output-ranges-equiv state))) :rule-classes :congruence)