• 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
      • Svex-compilation
        • Alias-normalization
        • Svex-design-flatten-and-normalize
        • Svex-design-compile
        • Svex-composition
          • Svex-compose-assigns-keys
          • Svex-compose*
          • Svex-compose
          • Svex-compose-svstack
          • Svex-assigns-compose1
          • Svex-assigns-compose
          • Svex-compose-bit-sccs
          • Svex-compose-assigns
          • Svex-replace-var
        • Compile.lisp
        • Assign->segment-drivers
        • Segment-driver-map-resolve
        • Assigns->segment-drivers
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svex-composition

Svex-compose-assigns

Compose together an alist of svex assignments, with no unrolling when variables depend on themselves.

Signature

(svex-compose-assigns assigns) → updates

Arguments

assigns — Guard (svex-alist-p assigns).

Returns

updates — Type (svex-alist-p updates).

Definitions and Theorems

Function: svex-compose-assigns

(defun svex-compose-assigns (assigns)
  (declare (xargs :guard (svex-alist-p assigns)))
  (let ((__function__ 'svex-compose-assigns))
    (declare (ignorable __function__))
    (b* (((mv updates memo)
          (with-fast-alist
               assigns
               (svex-compose-assigns-keys (svex-alist-keys assigns)
                                          assigns nil nil))))
      (fast-alist-free memo)
      updates)))

Theorem: svex-alist-p-of-svex-compose-assigns

(defthm svex-alist-p-of-svex-compose-assigns
  (b* ((updates (svex-compose-assigns assigns)))
    (svex-alist-p updates))
  :rule-classes :rewrite)

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

(defthm svex-compose-assigns-of-svex-alist-fix-assigns
  (equal (svex-compose-assigns (svex-alist-fix assigns))
         (svex-compose-assigns assigns)))

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

(defthm svex-compose-assigns-svex-alist-equiv-congruence-on-assigns
  (implies (svex-alist-equiv assigns assigns-equiv)
           (equal (svex-compose-assigns assigns)
                  (svex-compose-assigns assigns-equiv)))
  :rule-classes :congruence)