• 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

Sequential equivalence of aignets

We consider two aignets to be sequentially equivalent if:

• they have the same number of primary outputs
• corresponding outputs sequentially evaluate to the same value under the same series of primary input assignments and the all-0 initial register assignment.

This is a weaker condition than combinational equivalence: combinational equivalence implies sequential equivalence, but not vice versa.

This particular formulation of sequential equivalence assumes that evaluations of both networks start in the all-0 state. Why? Sequential equivalence should allow differences in the the state encoding of the two circuits, so we can't just universally quantify the initial register assignment. We could take the initial register assignments as two additional inputs, but then this wouldn't truly be an equivalence relation. We could existentially quantify over the initial register assignments, i.e.

there exist initial states for aignets A and B such that for all input sequences, the outputs of A and B have the same values on each frame

but this isn't really what we want either. It might instead be something like:

for each initial state of aignet A, there exists an initial state for aignet B such that for all input sequences, the outputs of A and B have the same values on each frame

but this isn't even an equivalence relation! Instead we're going to fix an initial state for each aignet, choosing the all-0 state as a simple convention. One can fix an FSM with a different initial state to one with the all-0 initial state using aignet-copy-init.

Definitions and Theorems

Theorem: seq-equiv-necc

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

Theorem: seq-equiv-is-an-equivalence

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

Theorem: seq-equiv-implies-equal-output-eval-seq-5

(defthm seq-equiv-implies-equal-output-eval-seq-5
  (implies (seq-equiv aignet aignet-equiv)
           (equal (output-eval-seq k n frames nil aignet)
                  (output-eval-seq k n frames nil aignet-equiv)))
  :rule-classes (:congruence))

Theorem: comb-equiv-implies-same-frame-regvals

(defthm comb-equiv-implies-same-frame-regvals
 (implies
      (and (comb-equiv aignet aignet2)
           (<= (num-regs aignet)
               (num-regs aignet2)))
      (bits-equiv (frame-regvals k frames initsts aignet)
                  (take (num-regs aignet)
                        (frame-regvals k frames initsts aignet2)))))

Theorem: comb-equiv-implies-seq-equiv

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