• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
        • Gatesimp
          • Gatesimp-p
          • !gatesimp->xor-mode
          • !gatesimp->level
          • !gatesimp->hashp
          • Gatesimp-fix
          • Gatesimp->xor-mode
          • Gatesimp->level
          • Gatesimp->hashp
        • Aignet-hash-mux
        • Aignet-hash-xor
        • Aignet-hash-and
        • Aignet-hash-or
        • Aignet-hash-iff
        • Aignet-build
        • Patbind-aignet-build
      • 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
      • 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

• Gatesimp

!gatesimp->level

Update the |AIGNET|::|LEVEL| field of a gatesimp bit structure.

Signature

(!gatesimp->level level x) → new-x

Arguments

level — Guard (gatesimp-level-p level).

x — Guard (gatesimp-p x).

Returns

new-x — Type (gatesimp-p new-x).

Definitions and Theorems

Function: !gatesimp->level

(defun !gatesimp->level (level x)
  (declare (xargs :guard (and (gatesimp-level-p level)
                              (gatesimp-p x))))
  (mbe :logic
       (b* ((level (mbe :logic (gatesimp-level-fix level)
                        :exec level))
            (x (gatesimp-fix x)))
         (part-install level x :width 3 :low 1))
       :exec (the (unsigned-byte 6)
                  (logior (the (unsigned-byte 6)
                               (logand (the (unsigned-byte 6) x)
                                       (the (signed-byte 5) -15)))
                          (the (unsigned-byte 4)
                               (ash (the (unsigned-byte 3) level)
                                    1))))))

Theorem: gatesimp-p-of-!gatesimp->level

(defthm gatesimp-p-of-!gatesimp->level
  (b* ((new-x (!gatesimp->level level x)))
    (gatesimp-p new-x))
  :rule-classes :rewrite)

Theorem: !gatesimp->level-of-gatesimp-level-fix-level

(defthm !gatesimp->level-of-gatesimp-level-fix-level
  (equal (!gatesimp->level (gatesimp-level-fix level)
                           x)
         (!gatesimp->level level x)))

Theorem: !gatesimp->level-gatesimp-level-equiv-congruence-on-level

(defthm !gatesimp->level-gatesimp-level-equiv-congruence-on-level
  (implies (gatesimp-level-equiv level level-equiv)
           (equal (!gatesimp->level level x)
                  (!gatesimp->level level-equiv x)))
  :rule-classes :congruence)

Theorem: !gatesimp->level-of-gatesimp-fix-x

(defthm !gatesimp->level-of-gatesimp-fix-x
  (equal (!gatesimp->level level (gatesimp-fix x))
         (!gatesimp->level level x)))

Theorem: !gatesimp->level-gatesimp-equiv-congruence-on-x

(defthm !gatesimp->level-gatesimp-equiv-congruence-on-x
  (implies (gatesimp-equiv x x-equiv)
           (equal (!gatesimp->level level x)
                  (!gatesimp->level level x-equiv)))
  :rule-classes :congruence)

Theorem: !gatesimp->level-is-gatesimp

(defthm !gatesimp->level-is-gatesimp
  (equal (!gatesimp->level level x)
         (change-gatesimp x :level level)))

Theorem: gatesimp->level-of-!gatesimp->level

(defthm gatesimp->level-of-!gatesimp->level
  (b* ((?new-x (!gatesimp->level level x)))
    (equal (gatesimp->level new-x)
           (gatesimp-level-fix level))))

Theorem: !gatesimp->level-equiv-under-mask

(defthm !gatesimp->level-equiv-under-mask
  (b* ((?new-x (!gatesimp->level level x)))
    (gatesimp-equiv-under-mask new-x x -15)))