• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
      • Faig-constructors
        • T-aig-ite*
        • F-aig-ite*
        • T-aig-ite
        • F-aig-ite
        • T-aig-tristate
        • F-aig-zif
        • T-aig-xor
        • T-aig-or
        • T-aig-iff
        • T-aig-and
        • F-aig-and
        • F-aig-xor
        • F-aig-or
        • F-aig-iff
        • F-aig-res
        • F-aig-unfloat
        • T-aig-not
        • F-aig-pullup
        • F-aig-not
        • T-aig-xdet
        • F-aig-xdet
      • Faig-onoff-equiv
      • Faig-purebool-p
      • Faig-alist-equiv
      • Faig-equiv
      • Faig-eval
      • Faig-restrict
      • Faig-fix
      • Faig-partial-eval
      • Faig-compose
      • Faig-compose-alist
      • Patbind-faig
      • Faig-constants
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Faig-constructors

T-aig-tristate

(t-aig-tristate c a) constructs an FAIG representing a tri-state buffer whose inputs are known to be non-X.

Signature

(t-aig-tristate c a) → *

See also 4v-tristate.

Onset of output:

(not (or (and (not c.on) c.off)
         (and c.on (not c.off) (not a.on) a.off)))

Offset of output:

(not (or (and (not c.on) c.off)
     (and c.on (not c.off) a.off (not a.on))))

Definitions and Theorems

Function: t-aig-tristate

(defun t-aig-tristate (c a)
  (declare (xargs :guard t))
  (let ((__function__ 't-aig-tristate))
    (declare (ignorable __function__))
    (b* (((faig a1 a0) a)
         ((faig c1 c0) c)
         (float (aig-and (aig-not c1) c0))
         (set (aig-and c1 (aig-not c0)))
         (on (aig-and (aig-not a0) a1))
         (off (aig-and (aig-not a1) a0)))
      (cons (aig-and (aig-not float)
                     (aig-not (aig-and set off)))
            (aig-and (aig-not float)
                     (aig-not (aig-and set on)))))))

Theorem: faig-eval-of-t-aig-tristate

(defthm faig-eval-of-t-aig-tristate
  (equal (faig-eval (t-aig-tristate c a) env)
         (t-aig-tristate (faig-eval c env)
                         (faig-eval a env))))

Theorem: faig-fix-equiv-implies-equal-t-aig-tristate-1

(defthm faig-fix-equiv-implies-equal-t-aig-tristate-1
  (implies (faig-fix-equiv c c-equiv)
           (equal (t-aig-tristate c a)
                  (t-aig-tristate c-equiv a)))
  :rule-classes (:congruence))

Theorem: faig-fix-equiv-implies-equal-t-aig-tristate-2

(defthm faig-fix-equiv-implies-equal-t-aig-tristate-2
  (implies (faig-fix-equiv a a-equiv)
           (equal (t-aig-tristate c a)
                  (t-aig-tristate c a-equiv)))
  :rule-classes (:congruence))

Theorem: faig-equiv-implies-faig-equiv-t-aig-tristate-2

(defthm faig-equiv-implies-faig-equiv-t-aig-tristate-2
  (implies (faig-equiv a a-equiv)
           (faig-equiv (t-aig-tristate c a)
                       (t-aig-tristate c a-equiv)))
  :rule-classes (:congruence))

Theorem: faig-equiv-implies-faig-equiv-t-aig-tristate-1

(defthm faig-equiv-implies-faig-equiv-t-aig-tristate-1
  (implies (faig-equiv c c-equiv)
           (faig-equiv (t-aig-tristate c a)
                       (t-aig-tristate c-equiv a)))
  :rule-classes (:congruence))