• Top

• Sv::vl-moddb.lisp

Vl-assign->svex-assign

Turn a VL assignment into an SVEX assignment or delayed assignment.

Signature

(vl-assign->svex-assign x ss scopes) → (mv vttree assigns)

Arguments

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

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

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

Returns

vttree — Type (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree)))) .

assigns — The assignment.
    Type (sv::assigns-p assigns).

This just straightforwardly converts the LHS and RHS to svex expressions, then converts the LHS into a sv::lhs-p.

At the moment we only support a single-tick delay, just because for a multi-tick we'd have to generate new names for the intermediate states.

Definitions and Theorems

Function: vl-assign->svex-assign

(defun vl-assign->svex-assign (x ss scopes)
 (declare (xargs :guard (and (vl-assign-p x)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-assign->svex-assign))
   (declare (ignorable __function__))
   (b*
     (((vl-assign x) (vl-assign-fix x))
      (vttree nil)
      ((when (vl-expr-case x.lvalue :vl-stream))
       (b* (((vmv vttree rhs ?rhs-type rhs-size)
             (vl-expr-to-svex-untyped x.expr ss scopes))
            ((unless rhs-size) (mv vttree nil))
            ((wvmv vttree delay :ctx x)
             (vl-maybe-gatedelay->delay x.delay))
            (rhs (if delay (sv::svex-add-delay rhs delay)
                   rhs))
            ((vmv vttree assigns)
             (vl-streaming-unpack-to-svex-assign-top
                  x.lvalue rhs x rhs-size ss scopes)))
         (mv vttree assigns)))
      ((vmv vttree lhs lhs-type :ctx x)
       (vl-expr-to-svex-lhs x.lvalue ss scopes))
      ((unless lhs-type) (mv vttree nil))
      ((wvmv vttree delay :ctx x)
       (vl-maybe-gatedelay->delay x.delay))
      ((vmv vttree type-err svex-rhs :ctx x)
       (vl-expr-to-svex-datatyped x.expr x.lvalue lhs-type ss scopes
                                  :compattype :assign))
      ((wvmv vttree :ctx x)
       (vl-type-error-basic-warn x.expr
                                 nil type-err x.lvalue lhs-type ss))
      ((when (not delay))
       (mv vttree
           (list (cons lhs
                       (sv::make-driver :value svex-rhs)))))
      (svex-rhs (sv::svex-add-delay svex-rhs delay)))
     (mv vttree
         (list (cons lhs
                     (sv::make-driver :value svex-rhs)))))))

Theorem: return-type-of-vl-assign->svex-assign.vttree

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

Theorem: assigns-p-of-vl-assign->svex-assign.assigns

(defthm assigns-p-of-vl-assign->svex-assign.assigns
  (b* (((mv ?vttree ?assigns)
        (vl-assign->svex-assign x ss scopes)))
    (sv::assigns-p assigns))
  :rule-classes :rewrite)

Theorem: vars-of-vl-assign->svex-assign-assigns

(defthm vars-of-vl-assign->svex-assign-assigns
  (b* (((mv ?vttree ?assigns)
        (vl-assign->svex-assign x ss scopes)))
    (sv::svarlist-addr-p (sv::assigns-vars assigns))))

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

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

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

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

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

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

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

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

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

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

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

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