		Search-engine friendly clone of the ACL2 documentation.

Aignet-comb-transforms

Abc-comb-simplify

Use the external tool ABC to apply a combinational simplification to the network, and assume the result correct.

Signature
(abc-comb-simplify input-aignet output-aignet config state) → (mv new-output-aignet new-state)
Arguments: config — Guard (abc-comb-simp-config-p config).

Definitions and Theorems

Function: abc-comb-simplify

(defun abc-comb-simplify (input-aignet output-aignet config state)
 (declare (xargs :stobjs (input-aignet output-aignet state)))
 (declare (xargs :guard (abc-comb-simp-config-p config)))
 (let ((__function__ 'abc-comb-simplify))
  (declare (ignorable __function__))
  (b*
   (((abc-comb-simp-config config))
    ((mv input-filename state)
     (oslib::tempfile "abc-comb-simplify-input.aig"))
    ((mv output-filename state)
     (oslib::tempfile "abc-comb-simplify-output.aig"))
    ((mv script-filename state)
     (oslib::tempfile "abc-comb-simplify-script"))
    ((unless (and input-filename
                  output-filename script-filename))
     (cw "Error -- couldn't generate temp filenames.~%")
     (b*
      ((output-aignet (aignet-raw-copy input-aignet output-aignet)))
      (mv output-aignet state)))
    (script (str::cat "&r " input-filename "; "
                      config.script "; &w " output-filename))
    ((local-stobjs frames)
     (mv output-aignet state frames))
    ((mv status output-aignet frames)
     (aignet-abc input-aignet output-aignet frames script
                 :script-filename script-filename
                 :input-filename input-filename
                 :output-filename output-filename
                 :axiom :comb-simp))
    ((when (stringp status))
     (cw "Error -- ABC failed: ~s0~%" status)
     (b*
      ((output-aignet (aignet-raw-copy input-aignet output-aignet)))
      (mv output-aignet state frames))))
   (mv output-aignet state frames))))

Theorem: normalize-inputs-of-abc-comb-simplify

(defthm normalize-inputs-of-abc-comb-simplify
 (implies
  (syntaxp (not (equal output-aignet ''nil)))
  (equal (abc-comb-simplify input-aignet output-aignet config state)
         (abc-comb-simplify input-aignet nil config state))))

Theorem: num-ins-of-abc-comb-simplify

(defthm num-ins-of-abc-comb-simplify
  (b* (((mv ?new-output-aignet ?new-state)
        (abc-comb-simplify input-aignet
                           output-aignet config state)))
    (equal (stype-count :pi new-output-aignet)
           (stype-count :pi input-aignet))))

Theorem: num-regs-of-abc-comb-simplify

(defthm num-regs-of-abc-comb-simplify
  (b* (((mv ?new-output-aignet ?new-state)
        (abc-comb-simplify input-aignet
                           output-aignet config state)))
    (equal (stype-count :reg new-output-aignet)
           (stype-count :reg input-aignet))))

Theorem: num-outs-of-abc-comb-simplify

(defthm num-outs-of-abc-comb-simplify
  (b* (((mv ?new-output-aignet ?new-state)
        (abc-comb-simplify input-aignet
                           output-aignet config state)))
    (equal (stype-count :po new-output-aignet)
           (stype-count :po input-aignet))))

Theorem: abc-comb-simplify-comb-equivalent

(defthm abc-comb-simplify-comb-equivalent
  (b* (((mv ?new-output-aignet ?new-state)
        (abc-comb-simplify input-aignet
                           output-aignet config state)))
    (comb-equiv new-output-aignet input-aignet)))

Theorem: w-state-of-abc-comb-simplify

(defthm w-state-of-abc-comb-simplify
  (b* (((mv ?new-output-aignet ?new-state)
        (abc-comb-simplify input-aignet
                           output-aignet config state)))
    (equal (w new-state) (w state))))

Subtopics

Abc-comb-simp-config: Configuration object for using the abc-comb-simplify transform on an aignet.
Abc-comb-simplify!: Like abc-comb-simplify, but overwrites the original network instead of returning a new one.