• 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
        • Compile.lisp
          • Svex-normalize-assigns
          • Svex-design-flatten
          • Svex-override-lhrange
          • Svex-override-lhs
          • Aliases-indexed->named-aux
          • Svex-compose-assigns/delays
          • Svex-alist-truncate-by-var-decls
          • Svar-map-truncate-by-var-decls
          • Aliases-to-var-decl-map-aux
          • Aliases-indexed->named
          • Svar-indexed->named-memo
          • Lhs-indexed->named
          • Svar-register-indnamememo
          • Svarlist-indexed->named
          • Maybe-svar-fix
          • Lhs-register-indnamememo
          • Maybe-indname-result
          • Aliases-to-var-decl-map
          • Svar-indexed->named
          • Aliases-boundedp-aux
          • Svex-apply-overrides
          • Indnamememo-to-var-decl-map
          • Indname-result
          • Assigns-compose
          • Delay-svarlist->delays
          • Indnamememo
          • Svex-override-vars
          • Delay-svar->delays
          • Assigns-to-overrides
          • Svarlist-collect-delays
          • Svex-overridelist-vars
          • Svex-overridelist-keys
          • Assigns-to-overrides-nrev
          • Var-decl-map
          • Cap-length
        • 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

• Compile.lisp

Svex-normalize-assigns

Signature

(svex-normalize-assigns assigns 
                        fixups constraints var-decls aliases) 
 
  → 
(mv res-assigns res-delays res-constraints)

Arguments

assigns — Guard (assigns-p assigns).

fixups — Guard (assigns-p fixups).

constraints — Guard (constraintlist-p constraints).

var-decls — Guard (var-decl-map-p var-decls).

Returns

res-assigns — Type (svex-alist-p res-assigns).

res-delays — Type (svex-alist-p res-delays).

res-constraints — Type (constraintlist-p res-constraints).

Definitions and Theorems

Function: svex-normalize-assigns

(defun svex-normalize-assigns
       (assigns fixups constraints var-decls aliases)
 (declare (xargs :stobjs (aliases)))
 (declare (xargs :guard (and (assigns-p assigns)
                             (assigns-p fixups)
                             (constraintlist-p constraints)
                             (var-decl-map-p var-decls))))
 (declare
  (xargs
    :guard (and (svarlist-boundedp (assigns-vars assigns)
                                   (aliass-length aliases))
                (svarlist-boundedp (assigns-vars fixups)
                                   (aliass-length aliases))
                (svarlist-boundedp (constraintlist-vars constraints)
                                   (aliass-length aliases)))))
 (let ((__function__ 'svex-normalize-assigns))
  (declare (ignorable __function__))
  (b*
   (((acl2::local-stobjs svexarr)
     (mv res-assigns
         res-delays res-constraints svexarr))
    (svexarr (resize-svexs (aliass-length aliases)
                           svexarr))
    (svexarr (cwtime (lhsarr-to-svexarr 0 aliases svexarr)))
    (norm-assigns (cwtime (assigns-subst assigns aliases svexarr)))
    (norm-fixups (cwtime (assigns-subst fixups aliases svexarr)))
    (norm-constraints (cwtime (constraintlist-subst-from-svexarr
                                   constraints aliases svexarr)))
    (net-assigns (cwtime (assigns->segment-drivers norm-assigns)))
    (res-assigns
         (make-fast-alist
              (cwtime (segment-driver-map-resolve net-assigns))))
    (final-fixups (assigns-compose norm-fixups res-assigns))
    (final-assigns1
     (fast-alist-free
      (fast-alist-clean
           (svex-apply-overrides (assigns-to-overrides final-fixups)
                                 res-assigns))))
    (final-assigns (svex-alist-truncate-by-var-decls
                        final-assigns1 var-decls nil))
    (delayvars
        (svarlist-collect-delays
             (svexlist-collect-vars (svex-alist-vals res-assigns))))
    (res-delays (delay-svarlist->delays delayvars))
    (trunc-delays
     (fast-alist-clean
        (svar-map-truncate-by-var-decls res-delays var-decls nil))))
   (mv final-assigns trunc-delays
       norm-constraints svexarr))))

Theorem: svex-alist-p-of-svex-normalize-assigns.res-assigns

(defthm svex-alist-p-of-svex-normalize-assigns.res-assigns
  (b*
   (((mv ?res-assigns
         ?res-delays ?res-constraints)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))
   (svex-alist-p res-assigns))
  :rule-classes :rewrite)

Theorem: svex-alist-p-of-svex-normalize-assigns.res-delays

(defthm svex-alist-p-of-svex-normalize-assigns.res-delays
  (b*
   (((mv ?res-assigns
         ?res-delays ?res-constraints)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))
   (svex-alist-p res-delays))
  :rule-classes :rewrite)

Theorem: constraintlist-p-of-svex-normalize-assigns.res-constraints

(defthm constraintlist-p-of-svex-normalize-assigns.res-constraints
  (b*
   (((mv ?res-assigns
         ?res-delays ?res-constraints)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))
   (constraintlist-p res-constraints))
  :rule-classes :rewrite)

Theorem: svex-normalize-assigns-of-assigns-fix-assigns

(defthm svex-normalize-assigns-of-assigns-fix-assigns
 (equal
     (svex-normalize-assigns (assigns-fix assigns)
                             fixups constraints var-decls aliases)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))

Theorem: svex-normalize-assigns-assigns-equiv-congruence-on-assigns

(defthm svex-normalize-assigns-assigns-equiv-congruence-on-assigns
 (implies
  (assigns-equiv assigns assigns-equiv)
  (equal
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)
     (svex-normalize-assigns assigns-equiv
                             fixups constraints var-decls aliases)))
 :rule-classes :congruence)

Theorem: svex-normalize-assigns-of-assigns-fix-fixups

(defthm svex-normalize-assigns-of-assigns-fix-fixups
 (equal
     (svex-normalize-assigns assigns (assigns-fix fixups)
                             constraints var-decls aliases)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))

Theorem: svex-normalize-assigns-assigns-equiv-congruence-on-fixups

(defthm svex-normalize-assigns-assigns-equiv-congruence-on-fixups
 (implies
  (assigns-equiv fixups fixups-equiv)
  (equal
       (svex-normalize-assigns assigns
                               fixups constraints var-decls aliases)
       (svex-normalize-assigns assigns fixups-equiv
                               constraints var-decls aliases)))
 :rule-classes :congruence)

Theorem: svex-normalize-assigns-of-constraintlist-fix-constraints

(defthm svex-normalize-assigns-of-constraintlist-fix-constraints
 (equal
     (svex-normalize-assigns assigns
                             fixups (constraintlist-fix constraints)
                             var-decls aliases)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))

Theorem: svex-normalize-assigns-constraintlist-equiv-congruence-on-constraints

(defthm
 svex-normalize-assigns-constraintlist-equiv-congruence-on-constraints
 (implies
  (constraintlist-equiv constraints constraints-equiv)
  (equal
      (svex-normalize-assigns assigns
                              fixups constraints var-decls aliases)
      (svex-normalize-assigns assigns fixups
                              constraints-equiv var-decls aliases)))
 :rule-classes :congruence)

Theorem: svex-normalize-assigns-of-var-decl-map-fix-var-decls

(defthm svex-normalize-assigns-of-var-decl-map-fix-var-decls
 (equal
    (svex-normalize-assigns assigns fixups
                            constraints (var-decl-map-fix var-decls)
                            aliases)
    (svex-normalize-assigns assigns
                            fixups constraints var-decls aliases)))

Theorem: svex-normalize-assigns-var-decl-map-equiv-congruence-on-var-decls

(defthm
  svex-normalize-assigns-var-decl-map-equiv-congruence-on-var-decls
 (implies
  (var-decl-map-equiv var-decls var-decls-equiv)
  (equal
      (svex-normalize-assigns assigns
                              fixups constraints var-decls aliases)
      (svex-normalize-assigns assigns fixups
                              constraints var-decls-equiv aliases)))
 :rule-classes :congruence)

Theorem: svex-normalize-assigns-of-lhslist-fix-aliases

(defthm svex-normalize-assigns-of-lhslist-fix-aliases
 (equal
     (svex-normalize-assigns assigns fixups constraints
                             var-decls (lhslist-fix aliases))
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))

Theorem: svex-normalize-assigns-lhslist-equiv-congruence-on-aliases

(defthm svex-normalize-assigns-lhslist-equiv-congruence-on-aliases
 (implies
  (lhslist-equiv aliases aliases-equiv)
  (equal
      (svex-normalize-assigns assigns
                              fixups constraints var-decls aliases)
      (svex-normalize-assigns assigns fixups
                              constraints var-decls aliases-equiv)))
 :rule-classes :congruence)

Theorem: vars-of-svex-normalize-assigns

(defthm vars-of-svex-normalize-assigns
  (b*
   (((mv ?res-assigns
         ?res-delays ?res-constraints)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))
   (implies (svarlist-addr-p (aliases-vars aliases))
            (svarlist-addr-p (svex-alist-vars res-assigns)))))

Theorem: keys-of-svex-normalize-assigns

(defthm keys-of-svex-normalize-assigns
  (b*
   (((mv ?res-assigns
         ?res-delays ?res-constraints)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))
   (implies (svarlist-addr-p (aliases-vars aliases))
            (svarlist-addr-p (svex-alist-keys res-assigns)))))

Theorem: vars-of-svex-normalize-assigns-delays

(defthm vars-of-svex-normalize-assigns-delays
  (b*
   (((mv ?res-assigns
         ?res-delays ?res-constraints)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))
   (implies (svarlist-addr-p (aliases-vars aliases))
            (svarlist-addr-p (svex-alist-vars res-delays)))))

Theorem: vars-of-svex-normalize-assigns-delays-keys

(defthm vars-of-svex-normalize-assigns-delays-keys
  (b*
   (((mv ?res-assigns
         ?res-delays ?res-constraints)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))
   (implies (svarlist-addr-p (aliases-vars aliases))
            (svarlist-addr-p (svex-alist-keys res-delays)))))

Theorem: vars-of-svex-normalize-assigns-constraints

(defthm vars-of-svex-normalize-assigns-constraints
  (b*
   (((mv ?res-assigns
         ?res-delays ?res-constraints)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))
   (implies
        (svarlist-addr-p (aliases-vars aliases))
        (svarlist-addr-p (constraintlist-vars res-constraints)))))

Theorem: no-duplicate-keys-of-svex-normalize-assigns-assigns

(defthm no-duplicate-keys-of-svex-normalize-assigns-assigns
  (b*
   (((mv ?res-assigns
         ?res-delays ?res-constraints)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))
   (no-duplicatesp-equal (svex-alist-keys res-assigns))))

Theorem: no-duplicate-keys-of-svex-normalize-assigns-delays

(defthm no-duplicate-keys-of-svex-normalize-assigns-delays
  (b*
   (((mv ?res-assigns
         ?res-delays ?res-constraints)
     (svex-normalize-assigns assigns
                             fixups constraints var-decls aliases)))
   (no-duplicatesp-equal (svex-alist-keys res-delays))))