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

• 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)