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