• 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-assigns-compose

Given an alist mapping variables to assigned expressions, compose them together into full update functions.

Signature

(svex-assigns-compose x &key (rewrite 't) 
                      (scc-selfcompose-limit 'nil)) 
 
  → 
xx

Arguments

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

scc-selfcompose-limit — Guard (maybe-natp scc-selfcompose-limit).

Returns

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

Definitions and Theorems

Function: svex-assigns-compose-fn

(defun svex-assigns-compose-fn (x rewrite scc-selfcompose-limit)
 (declare (xargs :guard (and (svex-alist-p x)
                             (maybe-natp scc-selfcompose-limit))))
 (let ((__function__ 'svex-assigns-compose))
   (declare (ignorable __function__))
   (b*
    (((mv err ans)
      (svex-assigns-compose1
           x
           :rewrite rewrite
           :scc-selfcompose-limit scc-selfcompose-limit))
     (ans (if err (prog2$ (raise "~@0" err)
                          (svex-alist-fix x))
            ans))
     (final-ans
          (b* ((vars (svex-alist-keys x))
               (xes-alist (svarlist-x-subst vars)))
            (with-fast-alist
                 xes-alist
                 (svex-alist-compose-rw
                      ans
                      (make-svex-substconfig :simp (if rewrite 20 t)
                                             :alist xes-alist))))))
    final-ans)))

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

(defthm svex-alist-p-of-svex-assigns-compose
  (b*
    ((xx (svex-assigns-compose-fn x rewrite scc-selfcompose-limit)))
    (svex-alist-p xx))
  :rule-classes :rewrite)

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

(defthm netevalcomp-p-of-svex-assigns-compose
  (b*
   ((?xx (svex-assigns-compose-fn x rewrite scc-selfcompose-limit)))
   (netevalcomp-p xx x)))

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

(defthm svex-alist-keys-of-svex-assigns-compose
  (b*
   ((?xx (svex-assigns-compose-fn x rewrite scc-selfcompose-limit)))
   (set-equiv (svex-alist-keys xx)
              (svex-alist-keys x))))

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

(defthm svex-assigns-compose-fn-of-svex-alist-fix-x
  (equal (svex-assigns-compose-fn (svex-alist-fix x)
                                  rewrite scc-selfcompose-limit)
         (svex-assigns-compose-fn x rewrite scc-selfcompose-limit)))

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

(defthm svex-assigns-compose-fn-svex-alist-equiv-congruence-on-x
 (implies
  (svex-alist-equiv x x-equiv)
  (equal
   (svex-assigns-compose-fn x rewrite scc-selfcompose-limit)
   (svex-assigns-compose-fn x-equiv rewrite scc-selfcompose-limit)))
 :rule-classes :congruence)

Theorem: svex-assigns-compose-fn-of-maybe-natp-fix-scc-selfcompose-limit

(defthm
    svex-assigns-compose-fn-of-maybe-natp-fix-scc-selfcompose-limit
  (equal (svex-assigns-compose-fn
              x rewrite
              (acl2::maybe-natp-fix scc-selfcompose-limit))
         (svex-assigns-compose-fn x rewrite scc-selfcompose-limit)))

Theorem: svex-assigns-compose-fn-maybe-nat-equiv-congruence-on-scc-selfcompose-limit

(defthm
 svex-assigns-compose-fn-maybe-nat-equiv-congruence-on-scc-selfcompose-limit
 (implies
  (acl2::maybe-nat-equiv scc-selfcompose-limit
                         scc-selfcompose-limit-equiv)
  (equal
   (svex-assigns-compose-fn x rewrite scc-selfcompose-limit)
   (svex-assigns-compose-fn x rewrite scc-selfcompose-limit-equiv)))
 :rule-classes :congruence)