• 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

Comb-equiv

Combinational equivalence of aignets

Signature

(comb-equiv aignet aignet2) → *

We consider two aignets to be combinationally equivalent if:

• corresponding outputs evaluate to the same value under the same input/register assignment
• next-states of corresponding registers evaluate to the same value under the same input/register assignment.

Definitions and Theorems

Function: comb-equiv

(defun comb-equiv (aignet aignet2)
  (declare (xargs :stobjs (aignet aignet2)))
  (declare (xargs :guard t))
  (let ((__function__ 'comb-equiv))
    (declare (ignorable __function__))
    (and (ec-call (outs-comb-equiv aignet aignet2))
         (ec-call (nxsts-comb-equiv aignet aignet2)))))

Theorem: comb-equiv-necc

(defthm comb-equiv-necc
 (implies (comb-equiv aignet aignet2)
          (and (equal (equal (output-eval n invals regvals aignet)
                             (output-eval n invals regvals aignet2))
                      t)
               (equal (equal (nxst-eval n invals regvals aignet)
                             (nxst-eval n invals regvals aignet2))
                      t))))

Theorem: comb-equiv-necc-lit-eval

(defthm comb-equiv-necc-lit-eval
 (implies
  (comb-equiv aignet aignet2)
  (and
   (equal
      (equal (lit-eval (fanin 0 (lookup-stype n (po-stype) aignet))
                       invals regvals aignet)
             (lit-eval (fanin 0 (lookup-stype n (po-stype) aignet2))
                       invals regvals aignet2))
      t)
   (equal (equal (lit-eval (lookup-reg->nxst n aignet)
                           invals regvals aignet)
                 (lit-eval (lookup-reg->nxst n aignet2)
                           invals regvals aignet2))
          t))))

Theorem: comb-equiv-is-an-equivalence

(defthm comb-equiv-is-an-equivalence
  (and (booleanp (comb-equiv x y))
       (comb-equiv x x)
       (implies (comb-equiv x y)
                (comb-equiv y x))
       (implies (and (comb-equiv x y) (comb-equiv y z))
                (comb-equiv x z)))
  :rule-classes (:equivalence))

Theorem: comb-equiv-refines-outs-comb-equiv

(defthm comb-equiv-refines-outs-comb-equiv
  (implies (comb-equiv x y)
           (outs-comb-equiv x y))
  :rule-classes (:refinement))

Theorem: comb-equiv-refines-nxsts-comb-equiv

(defthm comb-equiv-refines-nxsts-comb-equiv
  (implies (comb-equiv x y)
           (nxsts-comb-equiv x y))
  :rule-classes (:refinement))

Theorem: id-eval-of-aignet-norm-aignet

(defthm id-eval-of-aignet-norm-aignet
  (equal (id-eval id invals regvals (aignet-norm aignet))
         (id-eval id invals regvals aignet)))

Theorem: id-eval-aignet-equiv-congruence-on-aignet

(defthm id-eval-aignet-equiv-congruence-on-aignet
  (implies (aignet-equiv aignet aignet-equiv)
           (equal (id-eval id invals regvals aignet)
                  (id-eval id invals regvals aignet-equiv)))
  :rule-classes :congruence)

Theorem: lit-eval-of-aignet-norm-aignet

(defthm lit-eval-of-aignet-norm-aignet
  (equal (lit-eval lit invals regvals (aignet-norm aignet))
         (lit-eval lit invals regvals aignet)))

Theorem: lit-eval-aignet-equiv-congruence-on-aignet

(defthm lit-eval-aignet-equiv-congruence-on-aignet
  (implies (aignet-equiv aignet aignet-equiv)
           (equal (lit-eval lit invals regvals aignet)
                  (lit-eval lit invals regvals aignet-equiv)))
  :rule-classes :congruence)

Theorem: eval-and-of-lits-of-aignet-norm-aignet

(defthm eval-and-of-lits-of-aignet-norm-aignet
  (equal (eval-and-of-lits lit1 lit2
                           invals regvals (aignet-norm aignet))
         (eval-and-of-lits lit1 lit2 invals regvals aignet)))

Theorem: eval-and-of-lits-aignet-equiv-congruence-on-aignet

(defthm eval-and-of-lits-aignet-equiv-congruence-on-aignet
 (implies
   (aignet-equiv aignet aignet-equiv)
   (equal (eval-and-of-lits lit1 lit2 invals regvals aignet)
          (eval-and-of-lits lit1 lit2 invals regvals aignet-equiv)))
 :rule-classes :congruence)

Theorem: eval-xor-of-lits-of-aignet-norm-aignet

(defthm eval-xor-of-lits-of-aignet-norm-aignet
  (equal (eval-xor-of-lits lit1 lit2
                           invals regvals (aignet-norm aignet))
         (eval-xor-of-lits lit1 lit2 invals regvals aignet)))

Theorem: eval-xor-of-lits-aignet-equiv-congruence-on-aignet

(defthm eval-xor-of-lits-aignet-equiv-congruence-on-aignet
 (implies
   (aignet-equiv aignet aignet-equiv)
   (equal (eval-xor-of-lits lit1 lit2 invals regvals aignet)
          (eval-xor-of-lits lit1 lit2 invals regvals aignet-equiv)))
 :rule-classes :congruence)

Theorem: output-eval-of-aignet-norm-aignet

(defthm output-eval-of-aignet-norm-aignet
  (equal (output-eval n invals regvals (aignet-norm aignet))
         (output-eval n invals regvals aignet)))

Theorem: output-eval-aignet-equiv-congruence-on-aignet

(defthm output-eval-aignet-equiv-congruence-on-aignet
  (implies (aignet-equiv aignet aignet-equiv)
           (equal (output-eval n invals regvals aignet)
                  (output-eval n invals regvals aignet-equiv)))
  :rule-classes :congruence)

Theorem: nxst-eval-of-aignet-norm-aignet

(defthm nxst-eval-of-aignet-norm-aignet
  (equal (nxst-eval n invals regvals (aignet-norm aignet))
         (nxst-eval n invals regvals aignet)))

Theorem: nxst-eval-aignet-equiv-congruence-on-aignet

(defthm nxst-eval-aignet-equiv-congruence-on-aignet
  (implies (aignet-equiv aignet aignet-equiv)
           (equal (nxst-eval n invals regvals aignet)
                  (nxst-eval n invals regvals aignet-equiv)))
  :rule-classes :congruence)

Theorem: aignet-equiv-refines-outs-comb-equiv

(defthm aignet-equiv-refines-outs-comb-equiv
  (implies (aignet-equiv x y)
           (outs-comb-equiv x y))
  :rule-classes (:refinement))

Theorem: aignet-equiv-refines-nxsts-comb-equiv

(defthm aignet-equiv-refines-nxsts-comb-equiv
  (implies (aignet-equiv x y)
           (nxsts-comb-equiv x y))
  :rule-classes (:refinement))

Theorem: aignet-equiv-refines-comb-equiv

(defthm aignet-equiv-refines-comb-equiv
  (implies (aignet-equiv x y)
           (comb-equiv x y))
  :rule-classes (:refinement))

Theorem: comb-equiv-of-node-list-fix-aignet

(defthm comb-equiv-of-node-list-fix-aignet
  (equal (comb-equiv (node-list-fix aignet)
                     aignet2)
         (comb-equiv aignet aignet2)))

Theorem: comb-equiv-node-list-equiv-congruence-on-aignet

(defthm comb-equiv-node-list-equiv-congruence-on-aignet
  (implies (node-list-equiv aignet aignet-equiv)
           (equal (comb-equiv aignet aignet2)
                  (comb-equiv aignet-equiv aignet2)))
  :rule-classes :congruence)

Theorem: comb-equiv-of-node-list-fix-aignet2

(defthm comb-equiv-of-node-list-fix-aignet2
  (equal (comb-equiv aignet (node-list-fix aignet2))
         (comb-equiv aignet aignet2)))

Theorem: comb-equiv-node-list-equiv-congruence-on-aignet2

(defthm comb-equiv-node-list-equiv-congruence-on-aignet2
  (implies (node-list-equiv aignet2 aignet2-equiv)
           (equal (comb-equiv aignet aignet2)
                  (comb-equiv aignet aignet2-equiv)))
  :rule-classes :congruence)