• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
      • Aignet-copy-init
      • Aignet-simplify-with-tracking
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
      • Aignet-simplify-marked
      • Aignet-complete-copy
      • Aignet-transforms
      • Aignet-eval
      • Semantics
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Aignet

Aignet-copy-init

Set the initial state of an FSM to the all-0 convention.

Some algorithms assume that an FSM's initial state is the one where all registers are 0. This normalizes an FSM that does not follow this convention into one that does. Given the aignet and an initial state vector, this produces a new aignet that has registers toggled so that when its initial value is 0, its sequential simulations produce the same values as the input aignet when its initial value is the specified vector:

Theorem: lit-eval-seq-of-aignet-copy-init

(defthm lit-eval-seq-of-aignet-copy-init
  (b* ((aignet2 (aignet-copy-init aignet initsts
                                  :gatesimp gatesimp)))
    (equal (lit-eval-seq k (fanin 0 (lookup-stype n :po aignet2))
                         frames nil aignet2)
           (lit-eval-seq k (fanin 0 (lookup-stype n :po aignet))
                         frames initsts aignet))))

This operation is similar to aignet-complete-copy.

Definitions and Theorems

Function: aignet-copy-init-aux

(defun aignet-copy-init-aux
       (aignet initsts copy gatesimp strash aignet2)
 (declare (xargs :stobjs (aignet initsts copy strash aignet2)))
 (declare (xargs :guard (gatesimp-p gatesimp)))
 (declare (xargs :guard (<= (num-regs aignet)
                            (bits-length initsts))))
 (let ((__function__ 'aignet-copy-init-aux))
  (declare (ignorable __function__))
  (b*
   ((aignet2 (aignet-init (num-outs aignet)
                          (num-regs aignet)
                          (num-ins aignet)
                          (num-fanins aignet)
                          aignet2))
    (copy (resize-lits 0 copy))
    (strash (mbe :logic (non-exec '(nil))
                 :exec (strashtab-init (num-gates aignet)
                                       nil nil strash)))
    (copy (resize-lits (num-fanins aignet) copy))
    ((mv copy aignet2)
     (aignet-copy-ins aignet copy aignet2))
    (aignet2 (aignet-add-regs (num-regs aignet)
                              aignet2))
    (copy (aignet-copy-set-regs-init 0 aignet initsts copy aignet2))
    ((mv copy strash aignet2)
     (aignet-copy-comb aignet copy gatesimp strash aignet2))
    (aignet2 (aignet-copy-outs aignet copy aignet2))
    (aignet2 (aignet-copy-nxsts-init aignet initsts copy aignet2)))
   (mv copy strash aignet2))))

Theorem: normalize-aignet-copy-inits-aux

(defthm normalize-aignet-copy-inits-aux
 (implies
  (syntaxp (not (and (equal copy ''nil)
                     (equal strash ''(nil))
                     (equal aignet2 ''nil))))
  (equal (aignet-copy-init-aux aignet
                               initsts copy gatesimp strash aignet2)
         (aignet-copy-init-aux aignet initsts nil gatesimp '(nil)
                               nil))))

Theorem: num-outs-of-aignet-copy-init-aux

(defthm num-outs-of-aignet-copy-init-aux
 (equal
  (stype-count
   :po
   (mv-nth
       2
       (aignet-copy-init-aux aignet
                             initsts copy gatesimp strash aignet2)))
  (stype-count :po aignet)))

Theorem: num-regs-of-aignet-copy-init-aux

(defthm num-regs-of-aignet-copy-init-aux
 (equal
  (stype-count
   :reg
   (mv-nth
       2
       (aignet-copy-init-aux aignet
                             initsts copy gatesimp strash aignet2)))
  (stype-count :reg aignet)))

Theorem: num-ins-of-aignet-copy-init-aux

(defthm num-ins-of-aignet-copy-init-aux
 (equal
  (stype-count
   :pi
   (mv-nth
       2
       (aignet-copy-init-aux aignet
                             initsts copy gatesimp strash aignet2)))
  (stype-count :pi aignet)))

Theorem: eval-output-of-aignet-copy-init-aux

(defthm eval-output-of-aignet-copy-init-aux
 (implies
   (< (nfix n) (num-outs aignet))
   (b*
     (((mv & & aignet2)
       (aignet-copy-init-aux aignet
                             initsts copy gatesimp strash aignet2)))
     (equal (lit-eval (fanin 0 (lookup-stype n (po-stype) aignet2))
                      invals regvals aignet2)
            (lit-eval (fanin 0 (lookup-stype n (po-stype) aignet))
                      invals (b-xor-lst initsts regvals)
                      aignet)))))

Theorem: eval-nxst-of-aignet-copy-init-aux

(defthm eval-nxst-of-aignet-copy-init-aux
 (implies
   (< (nfix n) (num-regs aignet))
   (b*
     (((mv & & aignet2)
       (aignet-copy-init-aux aignet
                             initsts copy gatesimp strash aignet2)))
     (equal (lit-eval (lookup-reg->nxst n aignet2)
                      invals regvals aignet2)
            (b-xor (nth n initsts)
                   (lit-eval (lookup-reg->nxst n aignet)
                             invals (b-xor-lst initsts regvals)
                             aignet))))))

Theorem: aignet-copy-init-aux-of-gatesimp-fix-gatesimp

(defthm aignet-copy-init-aux-of-gatesimp-fix-gatesimp
  (equal
       (aignet-copy-init-aux aignet
                             initsts copy (gatesimp-fix gatesimp)
                             strash aignet2)
       (aignet-copy-init-aux aignet
                             initsts copy gatesimp strash aignet2)))

Theorem: aignet-copy-init-aux-gatesimp-equiv-congruence-on-gatesimp

(defthm aignet-copy-init-aux-gatesimp-equiv-congruence-on-gatesimp
 (implies
  (gatesimp-equiv gatesimp gatesimp-equiv)
  (equal (aignet-copy-init-aux aignet
                               initsts copy gatesimp strash aignet2)
         (aignet-copy-init-aux aignet initsts
                               copy gatesimp-equiv strash aignet2)))
 :rule-classes :congruence)

Theorem: aignet-copy-init-aux-when-all-initsts-0

(defthm aignet-copy-init-aux-when-all-initsts-0
 (implies
  (not (member 1 initsts))
  (equal
   (aignet-copy-init-aux aignet
                         initsts copy gatesimp strash aignet2)
   (aignet-complete-copy-aux aignet copy gatesimp strash aignet2))))

Function: aignet-copy-init-fn

(defun aignet-copy-init-fn (aignet initsts gatesimp aignet2)
 (declare (xargs :stobjs (aignet initsts aignet2)))
 (declare (xargs :guard (gatesimp-p gatesimp)))
 (declare (xargs :guard (<= (num-regs aignet)
                            (bits-length initsts))))
 (let ((__function__ 'aignet-copy-init))
  (declare (ignorable __function__))
  (b* (((local-stobjs copy strash)
        (mv copy strash aignet2)))
   (mbe
    :logic
    (non-exec
        (aignet-copy-init-aux (node-list-fix aignet)
                              initsts copy gatesimp strash aignet2))
    :exec (aignet-copy-init-aux aignet initsts
                                copy gatesimp strash aignet2)))))

Theorem: normalize-aignet-copy-init

(defthm normalize-aignet-copy-init
  (implies (syntaxp (not (equal aignet2 ''nil)))
           (equal (aignet-copy-init aignet initsts
                                    :gatesimp gatesimp
                                    :aignet2 aignet2)
                  (aignet-copy-init aignet initsts
                                    :gatesimp gatesimp
                                    :aignet2 nil))))

Theorem: num-outs-of-aignet-copy-init

(defthm num-outs-of-aignet-copy-init
  (equal (stype-count :po (aignet-copy-init aignet initsts
                                            :gatesimp gatesimp))
         (stype-count :po aignet)))

Theorem: num-regs-of-aignet-copy-init

(defthm num-regs-of-aignet-copy-init
  (equal (stype-count :reg (aignet-copy-init aignet initsts
                                             :gatesimp gatesimp))
         (stype-count :reg aignet)))

Theorem: num-ins-of-aignet-copy-init

(defthm num-ins-of-aignet-copy-init
  (equal (stype-count :pi (aignet-copy-init aignet initsts
                                            :gatesimp gatesimp))
         (stype-count :pi aignet)))

Theorem: eval-output-of-aignet-copy-init

(defthm eval-output-of-aignet-copy-init
 (implies
    (< (nfix n) (num-outs aignet))
    (b* ((aignet2 (aignet-copy-init aignet initsts
                                    :gatesimp gatesimp)))
      (equal (lit-eval (fanin 0 (lookup-stype n (po-stype) aignet2))
                       invals regvals aignet2)
             (lit-eval (fanin 0 (lookup-stype n (po-stype) aignet))
                       invals (b-xor-lst initsts regvals)
                       aignet)))))

Theorem: eval-nxst-of-aignet-copy-init

(defthm eval-nxst-of-aignet-copy-init
  (implies
       (< (nfix n) (num-regs aignet))
       (b* ((aignet2 (aignet-copy-init aignet initsts
                                       :gatesimp gatesimp)))
         (equal (lit-eval (lookup-reg->nxst n aignet2)
                          invals regvals aignet2)
                (b-xor (nth n initsts)
                       (lit-eval (lookup-reg->nxst n aignet)
                                 invals (b-xor-lst initsts regvals)
                                 aignet))))))

Theorem: aignet-copy-init-when-all-initsts-0

(defthm aignet-copy-init-when-all-initsts-0
  (implies (not (member 1 initsts))
           (equal (aignet-copy-init aignet initsts
                                    :gatesimp gatesimp)
                  (aignet-complete-copy aignet
                                        :gatesimp gatesimp))))

Theorem: aignet-copy-init-fn-of-node-list-fix-aignet

(defthm aignet-copy-init-fn-of-node-list-fix-aignet
  (equal (aignet-copy-init-fn (node-list-fix aignet)
                              initsts gatesimp aignet2)
         (aignet-copy-init-fn aignet initsts gatesimp aignet2)))

Theorem: aignet-copy-init-fn-node-list-equiv-congruence-on-aignet

(defthm aignet-copy-init-fn-node-list-equiv-congruence-on-aignet
 (implies
  (node-list-equiv aignet aignet-equiv)
  (equal
       (aignet-copy-init-fn aignet initsts gatesimp aignet2)
       (aignet-copy-init-fn aignet-equiv initsts gatesimp aignet2)))
 :rule-classes :congruence)

Theorem: aignet-copy-init-fn-of-gatesimp-fix-gatesimp

(defthm aignet-copy-init-fn-of-gatesimp-fix-gatesimp
  (equal (aignet-copy-init-fn aignet initsts (gatesimp-fix gatesimp)
                              aignet2)
         (aignet-copy-init-fn aignet initsts gatesimp aignet2)))

Theorem: aignet-copy-init-fn-gatesimp-equiv-congruence-on-gatesimp

(defthm aignet-copy-init-fn-gatesimp-equiv-congruence-on-gatesimp
 (implies
  (gatesimp-equiv gatesimp gatesimp-equiv)
  (equal
       (aignet-copy-init-fn aignet initsts gatesimp aignet2)
       (aignet-copy-init-fn aignet initsts gatesimp-equiv aignet2)))
 :rule-classes :congruence)

Theorem: aignet-copy-init-fn-of-node-list-fix-aignet2

(defthm aignet-copy-init-fn-of-node-list-fix-aignet2
  (equal (aignet-copy-init-fn aignet initsts
                              gatesimp (node-list-fix aignet2))
         (aignet-copy-init-fn aignet initsts gatesimp aignet2)))

Theorem: aignet-copy-init-fn-node-list-equiv-congruence-on-aignet2

(defthm aignet-copy-init-fn-node-list-equiv-congruence-on-aignet2
 (implies
  (node-list-equiv aignet2 aignet2-equiv)
  (equal
       (aignet-copy-init-fn aignet initsts gatesimp aignet2)
       (aignet-copy-init-fn aignet initsts gatesimp aignet2-equiv)))
 :rule-classes :congruence)

Theorem: bits-equiv-implies-bits-equiv-b-xor-lst-1

(defthm bits-equiv-implies-bits-equiv-b-xor-lst-1
  (implies (bits-equiv a a-equiv)
           (bits-equiv (b-xor-lst a b)
                       (b-xor-lst a-equiv b)))
  :rule-classes (:congruence))

Theorem: bits-equiv-implies-bits-equiv-b-xor-lst-2

(defthm bits-equiv-implies-bits-equiv-b-xor-lst-2
  (implies (bits-equiv b b-equiv)
           (bits-equiv (b-xor-lst a b)
                       (b-xor-lst a b-equiv)))
  :rule-classes (:congruence))

Theorem: list-fix-under-nth-equiv

(defthm list-fix-under-nth-equiv
  (nth-equiv (acl2::list-fix x) x))

Theorem: b-xor-lst-twice

(defthm b-xor-lst-twice
  (bits-equiv (b-xor-lst x (b-xor-lst x y))
              y))

Theorem: take-of-b-xor-lst

(defthm take-of-b-xor-lst
  (bits-equiv (take n (b-xor-lst a (take n b)))
              (take n (b-xor-lst a b))))

Theorem: bits-equiv-implies-bits-equiv-take-2

(defthm bits-equiv-implies-bits-equiv-take-2
  (implies (bits-equiv x x-equiv)
           (bits-equiv (take n x)
                       (take n x-equiv)))
  :rule-classes (:congruence))

Theorem: frame-regvals-of-aignet-copy-init

(defthm frame-regvals-of-aignet-copy-init
  (bits-equiv
       (frame-regvals k frames nil
                      (aignet-copy-init aignet initsts
                                        :gatesimp gatesimp))
       (take (num-regs aignet)
             (b-xor-lst initsts
                        (frame-regvals k frames initsts aignet)))))

Theorem: lit-eval-seq-of-aignet-copy-init

(defthm lit-eval-seq-of-aignet-copy-init
  (b* ((aignet2 (aignet-copy-init aignet initsts
                                  :gatesimp gatesimp)))
    (equal (lit-eval-seq k (fanin 0 (lookup-stype n :po aignet2))
                         frames nil aignet2)
           (lit-eval-seq k (fanin 0 (lookup-stype n :po aignet))
                         frames initsts aignet))))

Theorem: output-eval-seq-of-aignet-copy-init

(defthm output-eval-seq-of-aignet-copy-init
  (b* ((aignet2 (aignet-copy-init aignet initsts
                                  :gatesimp gatesimp)))
    (equal (output-eval-seq k n frames nil aignet2)
           (output-eval-seq k n frames initsts aignet))))

Theorem: seq-equiv-init-of-aignet-copy-init

(defthm seq-equiv-init-of-aignet-copy-init
  (seq-equiv-init (aignet-copy-init aignet initsts
                                    :gatesimp gatesimp)
                  nil aignet initsts))

Theorem: seq-equiv-init-is-seq-equiv-of-aignet-copy-init

(defthm seq-equiv-init-is-seq-equiv-of-aignet-copy-init
  (equal (seq-equiv-init aignet initsts aignet2 initsts2)
         (seq-equiv (aignet-copy-init aignet initsts
                                      :aignet2 nil)
                    (aignet-copy-init aignet2 initsts2
                                      :aignet2 nil))))