• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
        • Svexlist-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Sv

Svex-compose-dfs

Compose together a network of svex assignments, stopping when a variable depends on itself.

Signature

(svex-compose-dfs x assigns updates memo stack) 
  → 
(mv x1 updates1 memo1)

Arguments

x — svex we're traversing.
    Guard (svex-p x).

assigns — alist of assign stmts.
    Guard (svex-alist-p assigns).

updates — alist of composed update fns.
    Guard (svex-alist-p updates).

memo — memo table for internal nodes.
    Guard (svex-svex-memo-p memo).

stack — alist of seen vars.
    Guard (alistp stack).

Returns

x1 — composition of x with other internal wires.
    Type (svex-p x1).

updates1 — extended update functions.
    Type (svex-alist-p updates1).

memo1 — extended memo table.
    Type (svex-svex-memo-p memo1).

Theorem: return-type-of-svex-compose-dfs.x1

(defthm return-type-of-svex-compose-dfs.x1
  (b* (((mv ?x1 ?updates1 ?memo1)
        (svex-compose-dfs x assigns updates memo stack)))
    (svex-p x1))
  :rule-classes :rewrite)

Theorem: return-type-of-svex-compose-dfs.updates1

(defthm return-type-of-svex-compose-dfs.updates1
  (b* (((mv ?x1 ?updates1 ?memo1)
        (svex-compose-dfs x assigns updates memo stack)))
    (svex-alist-p updates1))
  :rule-classes :rewrite)

Theorem: return-type-of-svex-compose-dfs.memo1

(defthm return-type-of-svex-compose-dfs.memo1
  (b* (((mv ?x1 ?updates1 ?memo1)
        (svex-compose-dfs x assigns updates memo stack)))
    (svex-svex-memo-p memo1))
  :rule-classes :rewrite)

Theorem: return-type-of-svexlist-compose-dfs.x1

(defthm return-type-of-svexlist-compose-dfs.x1
  (b* (((mv ?x1 ?updates1 ?memo1)
        (svexlist-compose-dfs x assigns updates memo stack)))
    (svexlist-p x1))
  :rule-classes :rewrite)

Theorem: return-type-of-svexlist-compose-dfs.updates1

(defthm return-type-of-svexlist-compose-dfs.updates1
  (b* (((mv ?x1 ?updates1 ?memo1)
        (svexlist-compose-dfs x assigns updates memo stack)))
    (svex-alist-p updates1))
  :rule-classes :rewrite)

Theorem: return-type-of-svexlist-compose-dfs.memo1

(defthm return-type-of-svexlist-compose-dfs.memo1
  (b* (((mv ?x1 ?updates1 ?memo1)
        (svexlist-compose-dfs x assigns updates memo stack)))
    (svex-svex-memo-p memo1))
  :rule-classes :rewrite)

Theorem: svex-compose-dfs-of-svex-fix-x

(defthm svex-compose-dfs-of-svex-fix-x
  (equal (svex-compose-dfs (svex-fix x)
                           assigns updates memo stack)
         (svex-compose-dfs x assigns updates memo stack)))

Theorem: svex-compose-dfs-of-svex-alist-fix-assigns

(defthm svex-compose-dfs-of-svex-alist-fix-assigns
  (equal (svex-compose-dfs x (svex-alist-fix assigns)
                           updates memo stack)
         (svex-compose-dfs x assigns updates memo stack)))

Theorem: svex-compose-dfs-of-svex-alist-fix-updates

(defthm svex-compose-dfs-of-svex-alist-fix-updates
  (equal (svex-compose-dfs x assigns (svex-alist-fix updates)
                           memo stack)
         (svex-compose-dfs x assigns updates memo stack)))

Theorem: svex-compose-dfs-of-svex-svex-memo-fix-memo

(defthm svex-compose-dfs-of-svex-svex-memo-fix-memo
  (equal (svex-compose-dfs x assigns
                           updates (svex-svex-memo-fix memo)
                           stack)
         (svex-compose-dfs x assigns updates memo stack)))

Theorem: svexlist-compose-dfs-of-svexlist-fix-x

(defthm svexlist-compose-dfs-of-svexlist-fix-x
  (equal (svexlist-compose-dfs (svexlist-fix x)
                               assigns updates memo stack)
         (svexlist-compose-dfs x assigns updates memo stack)))

Theorem: svexlist-compose-dfs-of-svex-alist-fix-assigns

(defthm svexlist-compose-dfs-of-svex-alist-fix-assigns
  (equal (svexlist-compose-dfs x (svex-alist-fix assigns)
                               updates memo stack)
         (svexlist-compose-dfs x assigns updates memo stack)))

Theorem: svexlist-compose-dfs-of-svex-alist-fix-updates

(defthm svexlist-compose-dfs-of-svex-alist-fix-updates
  (equal (svexlist-compose-dfs x assigns (svex-alist-fix updates)
                               memo stack)
         (svexlist-compose-dfs x assigns updates memo stack)))

Theorem: svexlist-compose-dfs-of-svex-svex-memo-fix-memo

(defthm svexlist-compose-dfs-of-svex-svex-memo-fix-memo
  (equal (svexlist-compose-dfs x assigns
                               updates (svex-svex-memo-fix memo)
                               stack)
         (svexlist-compose-dfs x assigns updates memo stack)))

Theorem: svex-compose-dfs-svex-equiv-congruence-on-x

(defthm svex-compose-dfs-svex-equiv-congruence-on-x
 (implies
      (svex-equiv x x-equiv)
      (equal (svex-compose-dfs x assigns updates memo stack)
             (svex-compose-dfs x-equiv assigns updates memo stack)))
 :rule-classes :congruence)

Theorem: svex-compose-dfs-svex-alist-equiv-congruence-on-assigns

(defthm svex-compose-dfs-svex-alist-equiv-congruence-on-assigns
 (implies
      (svex-alist-equiv assigns assigns-equiv)
      (equal (svex-compose-dfs x assigns updates memo stack)
             (svex-compose-dfs x assigns-equiv updates memo stack)))
 :rule-classes :congruence)

Theorem: svex-compose-dfs-svex-alist-equiv-congruence-on-updates

(defthm svex-compose-dfs-svex-alist-equiv-congruence-on-updates
 (implies
      (svex-alist-equiv updates updates-equiv)
      (equal (svex-compose-dfs x assigns updates memo stack)
             (svex-compose-dfs x assigns updates-equiv memo stack)))
 :rule-classes :congruence)

Theorem: svex-compose-dfs-svex-svex-memo-equiv-congruence-on-memo

(defthm svex-compose-dfs-svex-svex-memo-equiv-congruence-on-memo
 (implies
      (svex-svex-memo-equiv memo memo-equiv)
      (equal (svex-compose-dfs x assigns updates memo stack)
             (svex-compose-dfs x assigns updates memo-equiv stack)))
 :rule-classes :congruence)

Theorem: svexlist-compose-dfs-svexlist-equiv-congruence-on-x

(defthm svexlist-compose-dfs-svexlist-equiv-congruence-on-x
 (implies
  (svexlist-equiv x x-equiv)
  (equal (svexlist-compose-dfs x assigns updates memo stack)
         (svexlist-compose-dfs x-equiv assigns updates memo stack)))
 :rule-classes :congruence)

Theorem: svexlist-compose-dfs-svex-alist-equiv-congruence-on-assigns

(defthm svexlist-compose-dfs-svex-alist-equiv-congruence-on-assigns
 (implies
  (svex-alist-equiv assigns assigns-equiv)
  (equal (svexlist-compose-dfs x assigns updates memo stack)
         (svexlist-compose-dfs x assigns-equiv updates memo stack)))
 :rule-classes :congruence)

Theorem: svexlist-compose-dfs-svex-alist-equiv-congruence-on-updates

(defthm svexlist-compose-dfs-svex-alist-equiv-congruence-on-updates
 (implies
  (svex-alist-equiv updates updates-equiv)
  (equal (svexlist-compose-dfs x assigns updates memo stack)
         (svexlist-compose-dfs x assigns updates-equiv memo stack)))
 :rule-classes :congruence)

Theorem: svexlist-compose-dfs-svex-svex-memo-equiv-congruence-on-memo

(defthm svexlist-compose-dfs-svex-svex-memo-equiv-congruence-on-memo
 (implies
  (svex-svex-memo-equiv memo memo-equiv)
  (equal (svexlist-compose-dfs x assigns updates memo stack)
         (svexlist-compose-dfs x assigns updates memo-equiv stack)))
 :rule-classes :congruence)

Subtopics

Svexlist-compose-dfs