|
|
|---|
|
|
|
|---|
Apply combinational SAT sweeping (fraiging) to remove redundancies in the input network.
(fraig aignet aignet2 config state) → (mv new-aignet2 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
Function:
(defun fraig (aignet aignet2 config state) (declare (xargs :stobjs (aignet aignet2 state))) (declare (xargs :guard (fraig-config-p config))) (let ((__function__ 'fraig)) (declare (ignorable __function__)) (b* (((local-stobjs aignet-tmp) (mv aignet2 aignet-tmp state)) ((mv aignet-tmp state) (fraig-core aignet aignet-tmp config state)) (aignet2 (aignet-prune-comb aignet-tmp aignet2 (fraig-config->gatesimp config)))) (mv aignet2 aignet-tmp state))))
Theorem:
(defthm num-ins-of-fraig (b* (((mv ?new-aignet2 ?new-state) (fraig aignet aignet2 config state))) (equal (stype-count :pi new-aignet2) (stype-count :pi aignet))))
Theorem:
(defthm num-regs-of-fraig (b* (((mv ?new-aignet2 ?new-state) (fraig aignet aignet2 config state))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet))))
Theorem:
(defthm num-outs-of-fraig (b* (((mv ?new-aignet2 ?new-state) (fraig aignet aignet2 config state))) (equal (stype-count :po new-aignet2) (stype-count :po aignet))))
Theorem:
(defthm fraig-comb-equivalent (b* (((mv ?new-aignet2 ?new-state) (fraig aignet aignet2 config state))) (comb-equiv new-aignet2 aignet)))
Theorem:
(defthm normalize-input-of-fraig (implies (syntaxp (not (equal aignet2 ''nil))) (equal (fraig aignet aignet2 config state) (fraig aignet nil config state))))
Theorem:
(defthm w-state-of-fraig (b* (((mv ?new-aignet2 ?new-state) (fraig aignet aignet2 config state))) (equal (w new-state) (w state))))
Theorem:
(defthm fraig-of-fraig-config-fix-config (equal (fraig aignet aignet2 (fraig-config-fix config) state) (fraig aignet aignet2 config state)))
Theorem:
(defthm fraig-fraig-config-equiv-congruence-on-config (implies (fraig-config-equiv config config-equiv) (equal (fraig aignet aignet2 config state) (fraig aignet aignet2 config-equiv state))) :rule-classes :congruence)