		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-operandinfo-to-svex-select

Signature
(vl-operandinfo-to-svex-select x indices ss scopes) → (mv err select-expr paramval)
Arguments: x — Guard (vl-operandinfo-p x).; indices — Guard (sv::svexlist-p indices).; ss — Guard (vl-scopestack-p ss).; scopes — Guard (vl-elabscopes-p scopes).
Returns: err — Type (iff (vl-msg-p err) err).; select-expr — Type (implies (not err) (sv::svex-select-p select-expr)).; paramval — Value corresponds to the innermost nested variable of select-expr.
Type (sv::maybe-4vec-p paramval).

Definitions and Theorems

Function: vl-operandinfo-to-svex-select

(defun vl-operandinfo-to-svex-select (x indices ss scopes)
 (declare (xargs :guard (and (vl-operandinfo-p x)
                             (sv::svexlist-p indices)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (declare
      (xargs :guard (and (vl-operandinfo-usertypes-ok x)
                         (equal (len indices)
                                (vl-operandinfo-index-count x)))))
 (let ((__function__ 'vl-operandinfo-to-svex-select))
  (declare (ignorable __function__))
  (b*
   (((fun (fail err)) (mv err nil nil))
    ((mv err x indices)
     (vl-operandinfo-to-svex-preproc x indices))
    (indices (list-fix indices))
    ((when err) (fail err))
    ((vl-operandinfo x))
    ((unless (vl-hidtrace-resolved-p x.hidtrace))
     (fail (vmsg "Unresolved hid indices")))
    ((vl-hidstep decl) (car x.hidtrace))
    (decl-scopes (vl-elabscopes-traverse (rev decl.elabpath)
                                         scopes))
    (info (vl-elabscopes-item-info x.declname decl-scopes))
    (item (or info decl.item))
    ((mv err paramval)
     (b*
      (((when (eq (tag item) :vl-vardecl))
        (b* (((vl-vardecl item)))
          (mv nil (and item.constp item.constval))))
       ((when (member (tag item)
                      '(:vl-modinst :vl-interfaceport)))
        (mv nil nil))
       ((unless (eq (tag item) :vl-paramdecl))
        (mv
         (vmsg
          "Referenced name not referring to a variable, interface instance, or parameter")
         nil))
       (paramval (b* (((vl-paramdecl item)))
                   (vl-paramtype-case
                        item.type
                        :vl-explicitvalueparam item.type.final-value
                        :otherwise nil)))
       ((unless paramval)
        (mv (vmsg "Parameter value is not resolved")
            nil)))
      (mv nil paramval)))
    ((when err) (fail err))
    ((mv err base-svar)
     (vl-operandinfo-base-svar x ss
                               :strictp (not paramval)))
    ((when err) (fail err))
    (partsel-p (not (vl-partselect-case x.part :none)))
    (seltrace-indices (if partsel-p (cddr indices) indices))
    ((mv err seltrace-select)
     (vl-seltrace-to-svex-select x.seltrace seltrace-indices
                                 x.hidtype base-svar ss))
    ((when err) (fail err))
    ((unless partsel-p)
     (mv nil seltrace-select paramval))
    ((list base-svex width-svex) indices)
    (psel-width (sv::2vec->val (sv::svex-quote->val width-svex)))
    ((mv err psel-select)
     (vl-plusminus-partselect->svex
          seltrace-select
          (vl-seltrace-type x.seltrace x.hidtype)
          (vl-partselect->plusminus x.part)
          base-svex psel-width))
    ((when err) (fail err)))
   (mv nil psel-select paramval))))

Theorem: return-type-of-vl-operandinfo-to-svex-select.err

(defthm return-type-of-vl-operandinfo-to-svex-select.err
  (b* (((mv ?err ?select-expr ?paramval)
        (vl-operandinfo-to-svex-select x indices ss scopes)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-operandinfo-to-svex-select.select-expr

(defthm return-type-of-vl-operandinfo-to-svex-select.select-expr
  (b* (((mv ?err ?select-expr ?paramval)
        (vl-operandinfo-to-svex-select x indices ss scopes)))
    (implies (not err)
             (sv::svex-select-p select-expr)))
  :rule-classes :rewrite)

Theorem: maybe-4vec-p-of-vl-operandinfo-to-svex-select.paramval

(defthm maybe-4vec-p-of-vl-operandinfo-to-svex-select.paramval
  (b* (((mv ?err ?select-expr ?paramval)
        (vl-operandinfo-to-svex-select x indices ss scopes)))
    (sv::maybe-4vec-p paramval))
  :rule-classes :rewrite)

Theorem: vars-of-vl-operandinfo-to-svex-select

(defthm vars-of-vl-operandinfo-to-svex-select
  (b* (((mv ?err ?select-expr ?paramval)
        (vl-operandinfo-to-svex-select x indices ss scopes)))
    (implies
         (and (sv::svarlist-addr-p (sv::svexlist-vars indices))
              (not err))
         (sv::svarlist-addr-p (sv::svex-select-vars select-expr)))))

Theorem: vl-operandinfo-to-svex-select-of-vl-operandinfo-fix-x

(defthm vl-operandinfo-to-svex-select-of-vl-operandinfo-fix-x
  (equal (vl-operandinfo-to-svex-select (vl-operandinfo-fix x)
                                        indices ss scopes)
         (vl-operandinfo-to-svex-select x indices ss scopes)))

Theorem: vl-operandinfo-to-svex-select-vl-operandinfo-equiv-congruence-on-x

(defthm
 vl-operandinfo-to-svex-select-vl-operandinfo-equiv-congruence-on-x
 (implies
  (vl-operandinfo-equiv x x-equiv)
  (equal (vl-operandinfo-to-svex-select x indices ss scopes)
         (vl-operandinfo-to-svex-select x-equiv indices ss scopes)))
 :rule-classes :congruence)

Theorem: vl-operandinfo-to-svex-select-of-svexlist-fix-indices

(defthm vl-operandinfo-to-svex-select-of-svexlist-fix-indices
  (equal (vl-operandinfo-to-svex-select x (sv::svexlist-fix indices)
                                        ss scopes)
         (vl-operandinfo-to-svex-select x indices ss scopes)))

Theorem: vl-operandinfo-to-svex-select-svexlist-equiv-congruence-on-indices

(defthm
 vl-operandinfo-to-svex-select-svexlist-equiv-congruence-on-indices
 (implies
  (sv::svexlist-equiv indices indices-equiv)
  (equal (vl-operandinfo-to-svex-select x indices ss scopes)
         (vl-operandinfo-to-svex-select x indices-equiv ss scopes)))
 :rule-classes :congruence)

Theorem: vl-operandinfo-to-svex-select-of-vl-scopestack-fix-ss

(defthm vl-operandinfo-to-svex-select-of-vl-scopestack-fix-ss
 (equal
     (vl-operandinfo-to-svex-select x indices (vl-scopestack-fix ss)
                                    scopes)
     (vl-operandinfo-to-svex-select x indices ss scopes)))

Theorem: vl-operandinfo-to-svex-select-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-operandinfo-to-svex-select-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal (vl-operandinfo-to-svex-select x indices ss scopes)
         (vl-operandinfo-to-svex-select x indices ss-equiv scopes)))
 :rule-classes :congruence)

Theorem: vl-operandinfo-to-svex-select-of-vl-elabscopes-fix-scopes

(defthm vl-operandinfo-to-svex-select-of-vl-elabscopes-fix-scopes
  (equal (vl-operandinfo-to-svex-select
              x indices ss (vl-elabscopes-fix scopes))
         (vl-operandinfo-to-svex-select x indices ss scopes)))

Theorem: vl-operandinfo-to-svex-select-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-operandinfo-to-svex-select-vl-elabscopes-equiv-congruence-on-scopes
 (implies
  (vl-elabscopes-equiv scopes scopes-equiv)
  (equal (vl-operandinfo-to-svex-select x indices ss scopes)
         (vl-operandinfo-to-svex-select x indices ss scopes-equiv)))
 :rule-classes :congruence)