		Search-engine friendly clone of the ACL2 documentation.

Aignet-comb-transforms

Observability-fix

Transform the aignet so that some observability don't-care conditions don't affect the logical equivalence of nodes.

Signature
(observability-fix aignet aignet2 config state) → (mv new-aignet2 new-state)
Arguments: aignet — Input aignet.; aignet2 — New aignet -- will be emptied.; config — Settings for the transform.
Guard (observability-config-p config).

This is mainly intended to be used on a single-output aignet, and mainly as a precursor to fraiging. Settings for the transform can be tweaked using the config input, which is an observability-config object.

Suppose we have a single-output AIG whose function is A & B, and that A is a small, simple function and B a large, complicated function. Sometimes it is the case that within B there are nodes that are logically inequivalent, but are equivalent when A is assumed. We'd like to be able to apply fraiging and get rid of these redundancies. But they aren't strictly equivalent, just equivalent under an observability condition.

The observability transform detects such situations and applies the following transform, which restricts the inputs to B so that it only sees inputs satisfying A. This makes such observability-equivalent nodes truly equivalent and allows fraiging to collapse them together.

First, decompose the topmost AND in the output and sort conjuncts into small and large ones according to some thresholds. The small ones are conjoined together as A and the large ones as B. If no conjuncts are smaller enough, the transform exits without doing anything.

Next, find a satisfying assignment for A. (If it is unsatisfiable, the output is constant false.) For each combinational input i that is in the minimized satisfying assignment with value v, make a mux A ? i : v. Then replace the occurrences of these inputs in B with these muxes. Finally, conjoin this modified copy of B with A.

This provably produces a combinationally equivalent network, since B is only changed in cases where A does not hold:

Theorem: observability-fix-comb-equivalent

(defthm observability-fix-comb-equivalent
  (b* (((mv ?new-aignet2 ?new-state)
        (observability-fix aignet aignet2 config state)))
    (comb-equiv new-aignet2 aignet)))

Definitions and Theorems

Function: observability-fix

(defun observability-fix (aignet aignet2 config state)
 (declare (xargs :stobjs (aignet aignet2 state)))
 (declare (xargs :guard (observability-config-p config)))
 (let ((__function__ 'observability-fix))
  (declare (ignorable __function__))
  (b*
   (((local-stobjs aignet-tmp)
     (mv aignet2 aignet-tmp state))
    (aignet2 (aignet-raw-copy aignet aignet2))
    ((mv aignet-tmp aignet2 state)
     (observability-fix-core aignet2 aignet-tmp config state))
    (aignet2
       (aignet-prune-comb aignet-tmp aignet2
                          (observability-config->gatesimp config))))
   (mv aignet2 aignet-tmp state))))

Theorem: num-ins-of-observability-fix

(defthm num-ins-of-observability-fix
  (b* (((mv ?new-aignet2 ?new-state)
        (observability-fix aignet aignet2 config state)))
    (equal (stype-count :pi new-aignet2)
           (stype-count :pi aignet))))

Theorem: num-regs-of-observability-fix

(defthm num-regs-of-observability-fix
  (b* (((mv ?new-aignet2 ?new-state)
        (observability-fix aignet aignet2 config state)))
    (equal (stype-count :reg new-aignet2)
           (stype-count :reg aignet))))

Theorem: num-outs-of-observability-fix

(defthm num-outs-of-observability-fix
  (b* (((mv ?new-aignet2 ?new-state)
        (observability-fix aignet aignet2 config state)))
    (equal (stype-count :po new-aignet2)
           (stype-count :po aignet))))

Theorem: observability-fix-comb-equivalent

(defthm observability-fix-comb-equivalent
  (b* (((mv ?new-aignet2 ?new-state)
        (observability-fix aignet aignet2 config state)))
    (comb-equiv new-aignet2 aignet)))

Theorem: normalize-input-of-observability-fix

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

Theorem: w-state-of-observability-fix

(defthm w-state-of-observability-fix
  (b* (((mv ?new-aignet2 ?new-state)
        (observability-fix aignet aignet2 config state)))
    (equal (w new-state) (w state))))

Theorem: observability-fix-of-node-list-fix-aignet

(defthm observability-fix-of-node-list-fix-aignet
  (equal (observability-fix (node-list-fix aignet)
                            aignet2 config state)
         (observability-fix aignet aignet2 config state)))

Theorem: observability-fix-node-list-equiv-congruence-on-aignet

(defthm observability-fix-node-list-equiv-congruence-on-aignet
 (implies
      (node-list-equiv aignet aignet-equiv)
      (equal (observability-fix aignet aignet2 config state)
             (observability-fix aignet-equiv aignet2 config state)))
 :rule-classes :congruence)

Theorem: observability-fix-of-node-list-fix-aignet2

(defthm observability-fix-of-node-list-fix-aignet2
  (equal (observability-fix aignet (node-list-fix aignet2)
                            config state)
         (observability-fix aignet aignet2 config state)))

Theorem: observability-fix-node-list-equiv-congruence-on-aignet2

(defthm observability-fix-node-list-equiv-congruence-on-aignet2
 (implies
      (node-list-equiv aignet2 aignet2-equiv)
      (equal (observability-fix aignet aignet2 config state)
             (observability-fix aignet aignet2-equiv config state)))
 :rule-classes :congruence)

Theorem: observability-fix-of-observability-config-fix-config

(defthm observability-fix-of-observability-config-fix-config
  (equal (observability-fix aignet aignet2
                            (observability-config-fix config)
                            state)
         (observability-fix aignet aignet2 config state)))

Theorem: observability-fix-observability-config-equiv-congruence-on-config

(defthm
  observability-fix-observability-config-equiv-congruence-on-config
 (implies
      (observability-config-equiv config config-equiv)
      (equal (observability-fix aignet aignet2 config state)
             (observability-fix aignet aignet2 config-equiv state)))
 :rule-classes :congruence)

Subtopics

Observability-fix-hyps/concls
Observability-fix-input-copies
Observability-fixed-inputs
Observability-fixed-regs
Observability-fix-hyp/concl
Observability-fix-lit
M-assum-n-output-observability
Observability-fix-outs
Observability-fix-nxsts
Observability-split-supergate-aux
Observability-fix-core
Observability-split-supergate
Aignet-build-wide-and
Observability-config: Configuration object for the observability-fix aignet transform.
Observability-fix!: Like observability-fix, but overwrites the original network instead of returning a new one.
Observability-size-check
M-assum-n-output-observability-config: Configuration object for the m-assum-n-output-observability aignet transform.