• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
        • Vl-to-sv
        • Vl-design->sv-design
          • Vl-simpconfig
          • Vl-hierarchy-sv-translation
          • Vl-expr-svex-translation
          • Vl-design->svex-modalist
          • Vl-svstmt
            • Vl-svstmt.lisp
              • Vl-casestmt-violation-conds
              • Vl-caselist-none/multiple
              • Vl-elaborated-expr-consteval
              • Vl-always->svex
              • Vl-caseexprs->svex-test
              • Vl-always->svex-checks
              • Vl-implicitvalueparam-final-type
              • Vl-assignstmt->svstmts
              • Vl-fundecl-to-svex
              • Vl-evatomlist-delay-substitution
              • Vl-consteval
              • Vl-alwayslist->svex
              • Vl-index-expr-svex/size/type
              • Vl-vardecllist->svstmts
              • Sv::svex-alist->assigns
              • Vl-case-conservative-test-expr
              • Vl-evatomlist->svex
              • Vl-case-xcond-wrapper
              • Sv::constraintlist-maybe-rewrite-fixpoint
              • Vl-always-apply-trigger-to-updates
              • Vl-initiallist-size-warnings
              • Vl-initial-size-warnings
              • Vl-finallist-size-warnings
              • Vl-always->svex-latch-warnings
              • Vl-final-size-warnings
              • Sv::svarlist-masked-x-subst
              • Sv::svar->lhs-by-mask
              • Svstmt-config
              • Sv::svex-alist-unset-nonblocking
              • Sv::svar->lhs-by-size
              • Combine-mask-alists
              • Sv::svarlist-delay-subst
              • Vttree-constraints-to-svstmts
              • Sv::4vmask-alist-unset-nonblocking
              • Sv::svarlist-remove-delays
              • Vl-caselist->caseexprs
              • Vl-evatomlist-has-edge
        • Vl-to-sv-main
        • Vl-simplify-sv
        • Vl-user-paramsettings->unparam-names
        • Vl-user-paramsettings->modnames
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-svstmt.lisp

Vl-always->svex

Translate a combinational or latch-type always block into a set of SVEX expressions.

Signature

(vl-always->svex x ss scopes config) 
  → 
(mv warnings assigns constraints)

Arguments

x — Guard (vl-always-p x).

ss — Guard (vl-scopestack-p ss).

scopes — Guard (vl-elabscopes-p scopes).

config — Guard (vl-simpconfig-p config).

Returns

warnings — Type (vl-warninglist-p warnings).

assigns — Type (and (sv::assigns-p assigns) (sv::svarlist-addr-p (sv::assigns-vars assigns))) .

constraints — Type (sv::constraintlist-p constraints).

Definitions and Theorems

Function: vl-always->svex

(defun vl-always->svex (x ss scopes config)
 (declare (xargs :guard (and (vl-always-p x)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-always->svex))
  (declare (ignorable __function__))
  (b*
   ((warnings nil)
    ((vl-simpconfig config))
    ((vl-always x) (vl-always-fix x))
    ((wmv ok warnings stmt trigger trigger-subst
          :ctx x)
     (vl-always->svex-checks x ss scopes))
    ((unless ok) (mv warnings nil nil))
    ((wmv ok warnings svstmts :ctx x)
     (vl-stmt->svstmts
        stmt ss scopes
        (make-svstmt-config
             :nonblockingp t
             :uniquecase-conservative config.uniquecase-conservative
             :uniquecase-constraints config.uniquecase-constraints)
        nil))
    ((unless ok) (mv warnings nil nil))
    (locstring (vl-location-string x.loc))
    ((wmv ok warnings st constraints
          blkst-write-masks nbst-write-masks
          :ctx x)
     (time$
      (sv::svstmtlist-compile-top svstmts
                                  :sclimit config.sc-limit
                                  :nb-delayp nil)
      :mintime 1/2
      :msg
      "; vl-always->svex: compiling statement at ~s0: ~st sec, ~sa bytes~%"
      :args (list locstring)))
    ((unless ok) (mv warnings nil nil))
    ((sv::svstate st)
     (sv::svstate-clean st))
    (- (sv::svstack-free st.blkst))
    (st.blkst
         (make-fast-alist (sv::svstack-to-svex-alist st.blkst)))
    (st.nonblkst (sv::svex-alist-unset-nonblocking st.nonblkst))
    (blk-written-vars (sv::svex-alist-keys st.blkst))
    (nb-written-vars (sv::svex-alist-keys st.nonblkst))
    (both-written
         (acl2::hons-intersection blk-written-vars nb-written-vars))
    ((when both-written)
     (mv
      (warn
       :type :vl-always->svex-fail
       :msg
       "~a0: Variables written by both blocking and ~
                        nonblocking assignments: ~x1"
       :args (list x both-written))
      nil nil))
    (written-vars (append blk-written-vars nb-written-vars))
    (nb-read-vars (sv::svex-alist-vars st.nonblkst))
    (loc-of-interest nil)
    (- (and loc-of-interest
            (sneaky-save 'blkst st.blkst))
       (and loc-of-interest
            (sneaky-save 'nonblkst st.nonblkst)))
    (blkst-rw
     (time$
      (sv::svex-alist-maybe-rewrite-fixpoint
           st.blkst config.sv-simplify
           :verbosep config.sv-simplify-verbosep)
      :mintime (if loc-of-interest 0 1/2)
      :msg
      "; vl-always->svex at ~s0: rewriting blocking assignments: ~st sec, ~sa bytes~%"
      :args (list locstring)))
    (nbst-rw
     (time$
      (sv::svex-alist-maybe-rewrite-fixpoint
           st.nonblkst config.sv-simplify
           :verbosep config.sv-simplify-verbosep)
      :mintime (if loc-of-interest 0 1/2)
      :msg
      "; vl-always->svex at ~s0: rewriting nonblocking assignments: ~st sec, ~sa bytes~%"
      :args (list locstring)))
    (constraints-rw
     (time$
      (sv::constraintlist-maybe-rewrite-fixpoint
           constraints config.sv-simplify
           :verbosep config.sv-simplify-verbosep)
      :mintime (if loc-of-interest 0 1/2)
      :msg
      "; vl-always->svex at ~s0: rewriting constraints: ~st sec, ~sa bytes~%"
      :args (list locstring)))
    (read-masks
     (time$
        (sv::svexlist-mask-alist
             (append (sv::svex-alist-vals blkst-rw)
                     (sv::svex-alist-vals nbst-rw)))
        :mintime (if loc-of-interest 0 1/2)
        :msg
        "; vl-always->svex at ~s0: read masks: ~st sec, ~sa bytes~%"
        :args (list locstring)))
    (nbst-write-masks
         (make-fast-alist (sv::4vmask-alist-unset-nonblocking
                               (fast-alist-free nbst-write-masks))))
    (- (clear-memoize-table 'sv::svex-unset-nonblocking)
       (clear-memoize-table 'sv::svex-set-nonblocking))
    (write-masks
     (fast-alist-clean
          (combine-mask-alists blkst-write-masks nbst-write-masks)))
    (subst
         (if (eq x.type :vl-always-comb)
             (sv::svarlist-masked-x-subst written-vars write-masks)
           (sv::svarlist-delay-subst written-vars)))
    ((wmv warnings :ctx x)
     (if (eq x.type :vl-always-comb)
         (vl-always->svex-latch-warnings write-masks read-masks)
       warnings))
    ((with-fast subst))
    (blkst-subst (sv::svex-alist-compose blkst-rw subst))
    (nbst-subst (sv::svex-alist-compose nbst-rw subst))
    (constraints-subst
         (sv::constraintlist-compose constraints-rw subst))
    (nbst-trigger
     (if trigger
      (b*
       ((nb-delaysubst
             (append-without-guard
                  trigger-subst
                  (sv::svarlist-delay-subst nb-read-vars)))
        (nbst-subst2
           (with-fast-alist
                nb-delaysubst
                (sv::svex-alist-compose nbst-subst nb-delaysubst))))
       (vl-always-apply-trigger-to-updates trigger nbst-subst2))
      (if config.nb-latch-delay-hack
          (sv::svex-alist-add-delay nbst-subst 1)
        nbst-subst)))
    (blkst-trigger
        (if trigger
            (vl-always-apply-trigger-to-updates trigger blkst-subst)
          blkst-subst))
    (constraints-trigger
         (if trigger (sv::constraintlist-add-pathcond
                          trigger nil constraints-subst)
           constraints-subst))
    (updates (append nbst-trigger blkst-trigger))
    (- (and loc-of-interest
            (sneaky-save 'updates updates)))
    (- (and loc-of-interest (break$)))
    (updates-rw
     (time$
      (sv::svex-alist-maybe-rewrite-fixpoint
           updates config.sv-simplify
           :verbosep config.sv-simplify-verbosep)
      :mintime (if loc-of-interest 0 1/2)
      :msg
      "; vl-always->svex at ~s0: rewriting final updates: ~st sec, ~sa bytes~%"
      :args (list (vl-location-string x.loc))))
    (lhs-sizes (make-fast-alist
                    (sv::svstmtlist-lhs-var-sizes svstmts (list nil)
                                                  nil)))
    (assigns
        (sv::svex-alist->assigns updates-rw lhs-sizes write-masks)))
   (mv warnings assigns constraints-trigger))))

Theorem: vl-warninglist-p-of-vl-always->svex.warnings

(defthm vl-warninglist-p-of-vl-always->svex.warnings
  (b* (((mv ?warnings ?assigns ?constraints)
        (vl-always->svex x ss scopes config)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-always->svex.assigns

(defthm return-type-of-vl-always->svex.assigns
  (b* (((mv ?warnings ?assigns ?constraints)
        (vl-always->svex x ss scopes config)))
    (and (sv::assigns-p assigns)
         (sv::svarlist-addr-p (sv::assigns-vars assigns))))
  :rule-classes :rewrite)

Theorem: constraintlist-p-of-vl-always->svex.constraints

(defthm constraintlist-p-of-vl-always->svex.constraints
  (b* (((mv ?warnings ?assigns ?constraints)
        (vl-always->svex x ss scopes config)))
    (sv::constraintlist-p constraints))
  :rule-classes :rewrite)

Theorem: vars-of-vl-always->svex

(defthm vars-of-vl-always->svex
 (b* (((mv ?warnings ?assigns ?constraints)
       (vl-always->svex x ss scopes config)))
  (and
      (sv::svarlist-addr-p (sv::assigns-vars assigns))
      (sv::svarlist-addr-p (sv::constraintlist-vars constraints)))))

Theorem: vl-always->svex-of-vl-always-fix-x

(defthm vl-always->svex-of-vl-always-fix-x
  (equal (vl-always->svex (vl-always-fix x)
                          ss scopes config)
         (vl-always->svex x ss scopes config)))

Theorem: vl-always->svex-vl-always-equiv-congruence-on-x

(defthm vl-always->svex-vl-always-equiv-congruence-on-x
  (implies (vl-always-equiv x x-equiv)
           (equal (vl-always->svex x ss scopes config)
                  (vl-always->svex x-equiv ss scopes config)))
  :rule-classes :congruence)

Theorem: vl-always->svex-of-vl-scopestack-fix-ss

(defthm vl-always->svex-of-vl-scopestack-fix-ss
  (equal (vl-always->svex x (vl-scopestack-fix ss)
                          scopes config)
         (vl-always->svex x ss scopes config)))

Theorem: vl-always->svex-vl-scopestack-equiv-congruence-on-ss

(defthm vl-always->svex-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-always->svex x ss scopes config)
                  (vl-always->svex x ss-equiv scopes config)))
  :rule-classes :congruence)

Theorem: vl-always->svex-of-vl-elabscopes-fix-scopes

(defthm vl-always->svex-of-vl-elabscopes-fix-scopes
  (equal (vl-always->svex x ss (vl-elabscopes-fix scopes)
                          config)
         (vl-always->svex x ss scopes config)))

Theorem: vl-always->svex-vl-elabscopes-equiv-congruence-on-scopes

(defthm vl-always->svex-vl-elabscopes-equiv-congruence-on-scopes
  (implies (vl-elabscopes-equiv scopes scopes-equiv)
           (equal (vl-always->svex x ss scopes config)
                  (vl-always->svex x ss scopes-equiv config)))
  :rule-classes :congruence)

Theorem: vl-always->svex-of-vl-simpconfig-fix-config

(defthm vl-always->svex-of-vl-simpconfig-fix-config
  (equal (vl-always->svex x ss scopes (vl-simpconfig-fix config))
         (vl-always->svex x ss scopes config)))

Theorem: vl-always->svex-vl-simpconfig-equiv-congruence-on-config

(defthm vl-always->svex-vl-simpconfig-equiv-congruence-on-config
  (implies (vl-simpconfig-equiv config config-equiv)
           (equal (vl-always->svex x ss scopes config)
                  (vl-always->svex x ss scopes config-equiv)))
  :rule-classes :congruence)