• 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-checks

Checks that the always block is suitable for translating to svex, ~ and returns the body statement and eventcontrol.

Signature

(vl-always->svex-checks x ss scopes) 
  → 
(mv ok warnings stmt trigger trigger-subst)

Arguments

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

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

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

Returns

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

stmt — on success, the body of the always block, without any eventcontrol.
    Type (implies ok (vl-stmt-p stmt)).

trigger — If present, indicates a flop rather than a latch/combinational block.
    Type (and (iff (sv::svex-p trigger) trigger) (implies trigger (sv::svarlist-addr-p (sv::svex-vars trigger)))) .

trigger-subst — Type (and (sv::svex-alist-p trigger-subst) (sv::svarlist-addr-p (sv::svex-alist-vars trigger-subst)) (sv::svarlist-addr-p (sv::svex-alist-keys trigger-subst))) .

Definitions and Theorems

Function: vl-always->svex-checks

(defun vl-always->svex-checks (x ss scopes)
 (declare (xargs :guard (and (vl-always-p x)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-always->svex-checks))
  (declare (ignorable __function__))
  (b* (((vl-always x) (vl-always-fix x))
       (warnings nil))
   (case
    x.type
    ((:vl-always-comb :vl-always-latch)
     (mv t (ok) x.stmt nil nil))
    (otherwise
     (b*
      (((unless (and (eq (vl-stmt-kind x.stmt)
                         :vl-timingstmt)
                     (eq (tag (vl-timingstmt->ctrl x.stmt))
                         :vl-eventcontrol)))
        (mv
         nil
         (warn
          :type :vl-always->svex-fail
          :msg
          "We only support always and always_ff blocks ~
                             that have a sensitivity list."
          :args (list x))
         nil nil nil))
       ((vl-timingstmt x.stmt))
       ((when (or (vl-eventcontrol->starp x.stmt.ctrl)
                  (not (vl-evatomlist-has-edge
                            (vl-eventcontrol->atoms x.stmt.ctrl)))))
        (b* ((warnings
                  (if (eq x.type :vl-always-ff)
                      (warn :type :vl-always-ff-warning
                            :msg "Always_ff is not edge-triggered."
                            :args (list x))
                    (ok))))
          (mv t (ok) x.stmt.body nil nil)))
       ((wmv warnings trigger)
        (vl-evatomlist->svex (vl-eventcontrol->atoms x.stmt.ctrl)
                             ss scopes))
       ((wmv warnings trigger-subst)
        (vl-evatomlist-delay-substitution
             (vl-eventcontrol->atoms x.stmt.ctrl)
             t ss scopes)))
      (mv t warnings
          x.stmt.body trigger trigger-subst)))))))

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

(defthm vl-warninglist-p-of-vl-always->svex-checks.warnings
  (b* (((mv ?ok
            ?warnings ?stmt ?trigger ?trigger-subst)
        (vl-always->svex-checks x ss scopes)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-always->svex-checks.stmt

(defthm return-type-of-vl-always->svex-checks.stmt
  (b* (((mv ?ok
            ?warnings ?stmt ?trigger ?trigger-subst)
        (vl-always->svex-checks x ss scopes)))
    (implies ok (vl-stmt-p stmt)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-always->svex-checks.trigger

(defthm return-type-of-vl-always->svex-checks.trigger
  (b* (((mv ?ok
            ?warnings ?stmt ?trigger ?trigger-subst)
        (vl-always->svex-checks x ss scopes)))
    (and (iff (sv::svex-p trigger) trigger)
         (implies trigger
                  (sv::svarlist-addr-p (sv::svex-vars trigger)))))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-always->svex-checks.trigger-subst

(defthm return-type-of-vl-always->svex-checks.trigger-subst
  (b* (((mv ?ok
            ?warnings ?stmt ?trigger ?trigger-subst)
        (vl-always->svex-checks x ss scopes)))
    (and (sv::svex-alist-p trigger-subst)
         (sv::svarlist-addr-p (sv::svex-alist-vars trigger-subst))
         (sv::svarlist-addr-p (sv::svex-alist-keys trigger-subst))))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

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

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

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

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