• 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
        • Comb-equiv
        • Seq-equiv
        • Seq-equiv-init
        • Invals
        • Outs-comb-equiv
        • Nxsts-comb-equiv
      • 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

• Semantics

Seq-equiv-init

Sequential equivalence of aignets on a particular initial state

See seq-equiv. This variant additionally takes the initial state of each aignet as an argument, and requires that they always produce the same outputs when run starting at that initial state.

Definitions and Theorems

Definition: initsts2p

(defabsstobj initsts2
  :foundation acl2::bitarr$c
  :recognizer (initsts2p :logic acl2::bitarr$ap
                         :exec acl2::bitarr$cp)
  :creator (create-initsts2 :logic acl2::create-bitarr$a
                            :exec acl2::create-bitarr$c)
  :exports ((initsts2s-length :logic acl2::bits$a-length
                              :exec acl2::bits$c-length
                              :protect nil)
            (get-initsts2 :logic acl2::bits$ai
                          :exec acl2::bits$ci
                          :protect nil)
            (set-initsts2 :logic acl2::update-bits$ai
                          :exec acl2::update-bits$ci
                          :protect nil)
            (resize-initsts2s :logic acl2::resize-bits$a
                              :exec acl2::resize-bits$c
                              :protect nil))
  :congruent-to bitarr)

Definition: create-initsts2

(defabsstobj initsts2
  :foundation acl2::bitarr$c
  :recognizer (initsts2p :logic acl2::bitarr$ap
                         :exec acl2::bitarr$cp)
  :creator (create-initsts2 :logic acl2::create-bitarr$a
                            :exec acl2::create-bitarr$c)
  :exports ((initsts2s-length :logic acl2::bits$a-length
                              :exec acl2::bits$c-length
                              :protect nil)
            (get-initsts2 :logic acl2::bits$ai
                          :exec acl2::bits$ci
                          :protect nil)
            (set-initsts2 :logic acl2::update-bits$ai
                          :exec acl2::update-bits$ci
                          :protect nil)
            (resize-initsts2s :logic acl2::resize-bits$a
                              :exec acl2::resize-bits$c
                              :protect nil))
  :congruent-to bitarr)

Definition: initsts2s-length

(defabsstobj initsts2
  :foundation acl2::bitarr$c
  :recognizer (initsts2p :logic acl2::bitarr$ap
                         :exec acl2::bitarr$cp)
  :creator (create-initsts2 :logic acl2::create-bitarr$a
                            :exec acl2::create-bitarr$c)
  :exports ((initsts2s-length :logic acl2::bits$a-length
                              :exec acl2::bits$c-length
                              :protect nil)
            (get-initsts2 :logic acl2::bits$ai
                          :exec acl2::bits$ci
                          :protect nil)
            (set-initsts2 :logic acl2::update-bits$ai
                          :exec acl2::update-bits$ci
                          :protect nil)
            (resize-initsts2s :logic acl2::resize-bits$a
                              :exec acl2::resize-bits$c
                              :protect nil))
  :congruent-to bitarr)

Definition: get-initsts2

(defabsstobj initsts2
  :foundation acl2::bitarr$c
  :recognizer (initsts2p :logic acl2::bitarr$ap
                         :exec acl2::bitarr$cp)
  :creator (create-initsts2 :logic acl2::create-bitarr$a
                            :exec acl2::create-bitarr$c)
  :exports ((initsts2s-length :logic acl2::bits$a-length
                              :exec acl2::bits$c-length
                              :protect nil)
            (get-initsts2 :logic acl2::bits$ai
                          :exec acl2::bits$ci
                          :protect nil)
            (set-initsts2 :logic acl2::update-bits$ai
                          :exec acl2::update-bits$ci
                          :protect nil)
            (resize-initsts2s :logic acl2::resize-bits$a
                              :exec acl2::resize-bits$c
                              :protect nil))
  :congruent-to bitarr)

Definition: set-initsts2

(defabsstobj initsts2
  :foundation acl2::bitarr$c
  :recognizer (initsts2p :logic acl2::bitarr$ap
                         :exec acl2::bitarr$cp)
  :creator (create-initsts2 :logic acl2::create-bitarr$a
                            :exec acl2::create-bitarr$c)
  :exports ((initsts2s-length :logic acl2::bits$a-length
                              :exec acl2::bits$c-length
                              :protect nil)
            (get-initsts2 :logic acl2::bits$ai
                          :exec acl2::bits$ci
                          :protect nil)
            (set-initsts2 :logic acl2::update-bits$ai
                          :exec acl2::update-bits$ci
                          :protect nil)
            (resize-initsts2s :logic acl2::resize-bits$a
                              :exec acl2::resize-bits$c
                              :protect nil))
  :congruent-to bitarr)

Definition: resize-initsts2s

(defabsstobj initsts2
  :foundation acl2::bitarr$c
  :recognizer (initsts2p :logic acl2::bitarr$ap
                         :exec acl2::bitarr$cp)
  :creator (create-initsts2 :logic acl2::create-bitarr$a
                            :exec acl2::create-bitarr$c)
  :exports ((initsts2s-length :logic acl2::bits$a-length
                              :exec acl2::bits$c-length
                              :protect nil)
            (get-initsts2 :logic acl2::bits$ai
                          :exec acl2::bits$ci
                          :protect nil)
            (set-initsts2 :logic acl2::update-bits$ai
                          :exec acl2::update-bits$ci
                          :protect nil)
            (resize-initsts2s :logic acl2::resize-bits$a
                              :exec acl2::resize-bits$c
                              :protect nil))
  :congruent-to bitarr)

Theorem: seq-equiv-init-necc

(defthm seq-equiv-init-necc
 (implies
      (seq-equiv-init aignet initsts aignet2 initsts2)
      (equal (equal (output-eval-seq k n inframes initsts aignet)
                    (output-eval-seq k n inframes initsts2 aignet2))
             t)))

Theorem: comb-equiv-implies-seq-equiv-init

(defthm comb-equiv-implies-seq-equiv-init
  (implies (comb-equiv aignet aignet2)
           (seq-equiv-init aignet initvals aignet2 initvals)))