• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
          • Vl-follow-hidexpr
            • Vl-follow-hidexpr-aux
          • Vl-index-expr-typetrace
          • Vl-follow-scopeexpr
          • Vl-follow-hidexpr-dimscheck
          • Vl-datatype-resolve-selects
          • Vl-datatype-remove-dim
          • Vl-operandinfo
          • Vl-follow-hidexpr-dimcheck
          • Vl-follow-data-selects
          • Vl-follow-hidexpr-error
          • Vl-hidstep
          • Vl-scopestack-find-item/ss/path
          • Vl-follow-array-indices
          • Vl-scopecontext
          • Vl-datatype-set-unsigned
          • Vl-selstep
          • Vl-scopestack-find-elabpath
          • Vl-hid-prefix-for-subhid
          • Vl-find-structmember
          • Vl-select
          • Vl-scopeexpr-replace-hid
          • Vl-genblocklist-find-block
          • Vl-partselect-width
          • Vl-seltrace->indices
          • Vl-datatype->structmembers
          • Vl-hidexpr-resolved-p
          • Vl-operandinfo->indices
          • Vl-flatten-hidindex
          • Vl-subhid-p
          • Vl-seltrace-usertypes-ok
          • Vl-flatten-hidexpr
          • Vl-scopeexpr->hid
          • Vl-seltrace-index-count
          • Vl-operandinfo-usertypes-ok
          • Vl-operandinfo-index-count
          • Vl-datatype-dims-count
          • Vl-scopeexpr-index-count
          • Vl-hidexpr-index-count
          • Vl-usertype-lookup
          • Vl-hidindex-resolved-p
          • Vl-scopeexpr-resolved-p
          • Vl-selstep-usertypes-ok
          • Vl-hidtrace
          • Vl-seltrace
          • Vl-scopedef-interface-p
        • Filtering-by-name
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
        • Range-tools
        • Finding-by-name
        • Stmt-tools
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-follow-hidexpr

Vl-follow-hidexpr-aux

Core routine for following hierarchical identifiers.

Signature

(vl-follow-hidexpr-aux x trace 
                       ss &key strictp (elabpath 'elabpath) 
                       (origx 'origx)) 
 
  → 
(mv err new-trace tail)

Arguments

x — HID expression fragment that we are following.
    Guard (vl-hidexpr-p x).

trace — Accumulator for the trace until now.
    Guard (vl-hidtrace-p trace).

ss — Current scopestack we're working from.
    Guard (vl-scopestack-p ss).

strictp — Guard (booleanp strictp).

elabpath — Guard (vl-elabtraversal-p elabpath).

origx — Original version of X, for better error messages.
    Guard (vl-scopeexpr-p origx).

Returns

err — A vl-msg-p on any error.
    Type (iff (vl-msg-p err) err).

new-trace — On success, a nonempty trace that records all the items we went through to resolve this HID. The car of the trace is the final item and scopestack.
    Type (vl-hidtrace-p new-trace).

tail — Remainder of x after arriving at the declaration.
    Type (vl-hidexpr-p tail).

See vl-follow-hidexpr for detailed discussion. This -aux function does most of the work, but for instance it doesn't deal with top-level hierarchical identifiers.

Definitions and Theorems

Function: vl-follow-hidexpr-aux-fn

(defun vl-follow-hidexpr-aux-fn (x trace ss strictp elabpath origx)
 (declare (xargs :guard (and (vl-hidexpr-p x)
                             (vl-hidtrace-p trace)
                             (vl-scopestack-p ss)
                             (booleanp strictp)
                             (vl-elabtraversal-p elabpath)
                             (vl-scopeexpr-p origx))))
 (let ((__function__ 'vl-follow-hidexpr-aux))
  (declare (ignorable __function__))
  (b*
   ((trace (vl-hidtrace-fix trace))
    (x (vl-hidexpr-fix x))
    ((mv name1 indices rest kind)
     (vl-hidexpr-case x :end (mv x.name nil nil :end)
                      :dot
                      (b* (((vl-hidindex x.first)))
                        (mv x.first.name
                            x.first.indices x.rest :dot))))
    ((when (eq name1 :vl-$root))
     (mv
        (vl-follow-hidexpr-error (vmsg "$root is not yet supported")
                                 ss)
        trace x))
    ((mv item item-ss item-path)
     (vl-scopestack-find-item/ss/path name1 ss))
    ((unless item)
     (mv (vl-follow-hidexpr-error (vmsg "item not found")
                                  ss)
         trace x))
    (elabpath (vl-elabpaths-append item-path elabpath))
    ((when (or (eq (tag item) :vl-vardecl)
               (eq (tag item) :vl-paramdecl)
               (eq (tag item) :vl-genvar)))
     (b* ((trace (cons (make-vl-hidstep :name name1
                                        :item item
                                        :ss item-ss
                                        :elabpath elabpath)
                       trace)))
       (mv nil trace x)))
    (trace (cons (make-vl-hidstep :name name1
                                  :item item
                                  :index (car indices)
                                  :ss item-ss
                                  :elabpath elabpath)
                 trace))
    ((when (or (eq (tag item) :vl-fundecl)
               (eq (tag item) :vl-taskdecl)))
     (if (eq kind :end)
         (mv nil trace x)
       (mv (vl-follow-hidexpr-error
                (vmsg (if (eq (tag item) :vl-fundecl)
                          "hierarchical reference into function"
                        "hierarchical reference into task"))
                item-ss)
           trace x)))
    ((when (eq (tag item) :vl-dpiimport))
     (if (eq kind :end)
         (mv nil trace x)
       (mv (vl-follow-hidexpr-error
                (vmsg "hierarchical reference into DPI import")
                item-ss)
           trace x)))
    ((when (eq (tag item) :vl-modport))
     (if (eq kind :end)
         (mv nil trace x)
       (mv (vl-follow-hidexpr-error
                (vmsg "hierarchical reference into modport")
                item-ss)
           trace x)))
    ((when (eq (tag item) :vl-modinst))
     (b*
      (((vl-modinst item))
       (dims (and item.range
                  (list (vl-range->dimension item.range))))
       (ifacep
        (let ((def (vl-scopestack-find-definition item.modname ss)))
          (and def (vl-scopedef-interface-p def))))
       (err (vl-follow-hidexpr-dimscheck name1 indices dims
                                         :strictp strictp
                                         :direct-okp ifacep))
       ((when err)
        (mv (vl-follow-hidexpr-error err item-ss)
            trace x))
       ((when (eq kind :end)) (mv nil trace x))
       ((mv mod mod-ss)
        (vl-scopestack-find-definition/ss item.modname item-ss))
       ((unless mod)
        (mv (vl-follow-hidexpr-error
                 (vmsg "reference through missing module ~s0"
                       item.modname)
                 item-ss)
            trace x))
       (modtag (tag mod))
       ((when (eq modtag :vl-udp))
        (mv (vl-follow-hidexpr-error
                 (vmsg "reference through primitive ~s0"
                       item.modname)
                 item-ss)
            trace x))
       ((unless (or (eq modtag :vl-module)
                    (eq modtag :vl-interface)))
        (mv
         (vl-follow-hidexpr-error
             (vmsg "module instance ~s0 of ~s1: invalid type ~x2???"
                   name1 item.modname modtag)
             item-ss)
         trace x))
       (mod-path (list (vl-elabinstruction-push-named
                            (vl-elabkey-def item.modname))
                       (vl-elabinstruction-root)))
       (next-ss (vl-scopestack-push mod mod-ss)))
      (vl-follow-hidexpr-aux rest trace next-ss
                             :strictp strictp
                             :elabpath mod-path)))
    ((when (eq (tag item) :vl-interfaceport))
     (b*
      (((vl-interfaceport item))
       (err (vl-follow-hidexpr-dimscheck name1 indices item.udims
                                         :strictp strictp
                                         :direct-okp t))
       ((when err)
        (mv (vl-follow-hidexpr-error err item-ss)
            trace x))
       ((when (eq kind :end)) (mv nil trace x))
       ((mv iface iface-ss)
        (vl-scopestack-find-definition/ss item.ifname item-ss))
       ((unless iface)
        (mv (vl-follow-hidexpr-error
                 (vmsg "reference through missing interface ~s0"
                       item.ifname)
                 item-ss)
            trace x))
       (iftag (tag iface))
       ((unless (eq iftag :vl-interface))
        (mv
         (vl-follow-hidexpr-error
          (vmsg
           "interface port ~s0 of interface ~s1: invalid type ~x2???"
           name1 item.ifname iftag)
          item-ss)
         trace x))
       (next-ss (vl-scopestack-push iface iface-ss))
       (iface-path (list (vl-elabinstruction-push-named
                              (vl-elabkey-def item.ifname))
                         (vl-elabinstruction-root))))
      (vl-follow-hidexpr-aux rest trace next-ss
                             :strictp strictp
                             :elabpath iface-path)))
    ((when (eq (tag item) :vl-genbegin))
     (b*
      (((when (consp indices))
        (mv (vl-follow-hidexpr-error
                 "array indices on reference to generate block"
                 item-ss)
            trace x))
       ((when (eq kind :end))
        (mv (vl-follow-hidexpr-error
                 "reference to generate block" item-ss)
            trace x))
       (genblob (vl-sort-genelements
                     (vl-genblock->elems (vl-genbegin->block item))
                     :scopetype :vl-genblock
                     :id name1))
       (next-ss (vl-scopestack-push genblob item-ss))
       (next-path
        (cons
             (vl-elabinstruction-push-named (vl-elabkey-item name1))
             elabpath)))
      (vl-follow-hidexpr-aux rest trace next-ss
                             :strictp strictp
                             :elabpath next-path)))
    ((when (eq (tag item) :vl-genarray))
     (b*
      (((when (eq kind :end))
        (mv (vl-follow-hidexpr-error
                 "reference to generate array" item-ss)
            trace x))
       ((unless (consp indices))
        (mv
         (vl-follow-hidexpr-error
          "reference through generate array must have an array index"
          item-ss)
         trace x))
       ((unless (atom (rest indices)))
        (mv (vl-follow-hidexpr-error
                 "too many indices through generate array"
                 item-ss)
            trace x))
       (index-expr (first indices))
       ((unless (vl-expr-resolved-p index-expr))
        (mv (vl-follow-hidexpr-error
                 "unresolved index into generate array"
                 item-ss)
            trace x))
       (blocknum (vl-resolved->val index-expr))
       (block (vl-genblocklist-find-block
                   blocknum (vl-genarray->blocks item)))
       ((unless block)
        (mv (vl-follow-hidexpr-error
                 (vmsg "invalid index into generate array: ~x0"
                       blocknum)
                 item-ss)
            trace x))
       (array-scope (vl-sort-genelements nil
                                         :scopetype :vl-genarray
                                         :id name1))
       (block-scope
            (vl-sort-genelements (vl-genblock->elems block)
                                 :scopetype :vl-genarrayblock
                                 :id blocknum))
       (next-ss (vl-scopestack-push
                     block-scope
                     (vl-scopestack-push array-scope item-ss)))
       (next-path
        (list*
         (vl-elabinstruction-push-named (vl-elabkey-index blocknum))
         (vl-elabinstruction-push-named (vl-elabkey-item name1))
         elabpath)))
      (vl-follow-hidexpr-aux rest trace next-ss
                             :strictp strictp
                             :elabpath next-path)))
    ((when (eq (tag item) :vl-typedef))
     (b* (((when (eq kind :end))
           (mv nil trace x)))
       (mv (vl-follow-hidexpr-error
                "hierarchical reference through typedef"
                item-ss)
           trace x)))
    ((when (or (eq (tag item) :vl-genif)
               (eq (tag item) :vl-gencase)
               (eq (tag item) :vl-genloop)
               (eq (tag item) :vl-genbase)))
     (mv
      (vl-follow-hidexpr-error (vmsg "hierarchical reference to ~x0"
                                     (tag item))
                               item-ss)
      trace x))
    ((when (eq (tag item) :vl-gateinst))
     (mv (vl-follow-hidexpr-error
              "hierarchical reference to gate instance"
              item-ss)
         trace x)))
   (mv (impossible) trace x))))

Theorem: return-type-of-vl-follow-hidexpr-aux.err

(defthm return-type-of-vl-follow-hidexpr-aux.err
  (b*
    (((mv ?err ?new-trace set::?tail)
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: vl-hidtrace-p-of-vl-follow-hidexpr-aux.new-trace

(defthm vl-hidtrace-p-of-vl-follow-hidexpr-aux.new-trace
  (b*
    (((mv ?err ?new-trace set::?tail)
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))
    (vl-hidtrace-p new-trace))
  :rule-classes :rewrite)

Theorem: vl-hidexpr-p-of-vl-follow-hidexpr-aux.tail

(defthm vl-hidexpr-p-of-vl-follow-hidexpr-aux.tail
  (b*
    (((mv ?err ?new-trace set::?tail)
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))
    (vl-hidexpr-p tail))
  :rule-classes :rewrite)

Theorem: consp-of-vl-follow-hidexpr-aux.new-trace

(defthm consp-of-vl-follow-hidexpr-aux.new-trace
  (b*
    (((mv ?err ?new-trace set::?tail)
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))
    (implies (or (consp trace) (not err))
             (consp new-trace)))
  :rule-classes :rewrite)

Theorem: vl-follow-hidexpr-no-index-on-first

(defthm vl-follow-hidexpr-no-index-on-first
  (b*
    (((mv ?err ?new-trace set::?tail)
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))
    (implies (not err)
             (not (vl-hidstep->index (car new-trace))))))

Theorem: context-irrelevance-of-vl-follow-hidexpr-aux

(defthm context-irrelevance-of-vl-follow-hidexpr-aux
 (implies
  (syntaxp
   (not
    (equal
        origx
        (list 'quote
              (with-guard-checking :none (vl-scopeexpr-fix nil))))))
  (b* (((mv err1 trace1 tail1)
        (vl-follow-hidexpr-aux x trace ss
                               :elabpath elabpath
                               :strictp strictp
                               :origx origx))
       ((mv err2 trace2 tail2)
        (vl-follow-hidexpr-aux x trace ss
                               :elabpath elabpath
                               :strictp strictp
                               :origx (vl-scopeexpr-fix nil))))
    (and (equal trace1 trace2)
         (equal tail1 tail2)
         (iff err1 err2)))))

Theorem: count-of-vl-follow-hidexpr-aux.tail

(defthm count-of-vl-follow-hidexpr-aux.tail
  (b*
    (((mv ?err ?new-trace set::?tail)
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))
    (<= (vl-hidexpr-count tail)
        (vl-hidexpr-count x)))
  :rule-classes :linear)

Theorem: vl-subhid-p-of-vl-follow-hidexpr-aux

(defthm vl-subhid-p-of-vl-follow-hidexpr-aux
  (b*
    (((mv ?err ?new-trace set::?tail)
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))
    (implies (not err)
             (vl-subhid-p tail x))))

Theorem: vl-follow-hidexpr-aux-fn-of-vl-hidexpr-fix-x

(defthm vl-follow-hidexpr-aux-fn-of-vl-hidexpr-fix-x
 (equal
      (vl-follow-hidexpr-aux-fn (vl-hidexpr-fix x)
                                trace ss strictp elabpath origx)
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))

Theorem: vl-follow-hidexpr-aux-fn-vl-hidexpr-equiv-congruence-on-x

(defthm vl-follow-hidexpr-aux-fn-vl-hidexpr-equiv-congruence-on-x
 (implies
   (vl-hidexpr-equiv x x-equiv)
   (equal
        (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)
        (vl-follow-hidexpr-aux-fn x-equiv
                                  trace ss strictp elabpath origx)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-aux-fn-of-vl-hidtrace-fix-trace

(defthm vl-follow-hidexpr-aux-fn-of-vl-hidtrace-fix-trace
 (equal
      (vl-follow-hidexpr-aux-fn x (vl-hidtrace-fix trace)
                                ss strictp elabpath origx)
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))

Theorem: vl-follow-hidexpr-aux-fn-vl-hidtrace-equiv-congruence-on-trace

(defthm
     vl-follow-hidexpr-aux-fn-vl-hidtrace-equiv-congruence-on-trace
 (implies
   (vl-hidtrace-equiv trace trace-equiv)
   (equal
        (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)
        (vl-follow-hidexpr-aux-fn
             x
             trace-equiv ss strictp elabpath origx)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-aux-fn-of-vl-scopestack-fix-ss

(defthm vl-follow-hidexpr-aux-fn-of-vl-scopestack-fix-ss
 (equal
      (vl-follow-hidexpr-aux-fn x trace (vl-scopestack-fix ss)
                                strictp elabpath origx)
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))

Theorem: vl-follow-hidexpr-aux-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
      vl-follow-hidexpr-aux-fn-vl-scopestack-equiv-congruence-on-ss
 (implies
   (vl-scopestack-equiv ss ss-equiv)
   (equal
        (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)
        (vl-follow-hidexpr-aux-fn
             x
             trace ss-equiv strictp elabpath origx)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-aux-fn-of-bool-fix-strictp

(defthm vl-follow-hidexpr-aux-fn-of-bool-fix-strictp
 (equal
      (vl-follow-hidexpr-aux-fn x trace ss (acl2::bool-fix strictp)
                                elabpath origx)
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))

Theorem: vl-follow-hidexpr-aux-fn-iff-congruence-on-strictp

(defthm vl-follow-hidexpr-aux-fn-iff-congruence-on-strictp
 (implies
   (iff strictp strictp-equiv)
   (equal
        (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)
        (vl-follow-hidexpr-aux-fn
             x
             trace ss strictp-equiv elabpath origx)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-aux-fn-of-vl-elabtraversal-fix-elabpath

(defthm vl-follow-hidexpr-aux-fn-of-vl-elabtraversal-fix-elabpath
 (equal
   (vl-follow-hidexpr-aux-fn x trace ss
                             strictp (vl-elabtraversal-fix elabpath)
                             origx)
   (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))

Theorem: vl-follow-hidexpr-aux-fn-vl-elabtraversal-equiv-congruence-on-elabpath

(defthm
 vl-follow-hidexpr-aux-fn-vl-elabtraversal-equiv-congruence-on-elabpath
 (implies
   (vl-elabtraversal-equiv elabpath elabpath-equiv)
   (equal
        (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)
        (vl-follow-hidexpr-aux-fn
             x
             trace ss strictp elabpath-equiv origx)))
 :rule-classes :congruence)

Theorem: vl-follow-hidexpr-aux-fn-of-vl-scopeexpr-fix-origx

(defthm vl-follow-hidexpr-aux-fn-of-vl-scopeexpr-fix-origx
 (equal
      (vl-follow-hidexpr-aux-fn x trace ss strictp
                                elabpath (vl-scopeexpr-fix origx))
      (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)))

Theorem: vl-follow-hidexpr-aux-fn-vl-scopeexpr-equiv-congruence-on-origx

(defthm
    vl-follow-hidexpr-aux-fn-vl-scopeexpr-equiv-congruence-on-origx
 (implies
   (vl-scopeexpr-equiv origx origx-equiv)
   (equal
        (vl-follow-hidexpr-aux-fn x trace ss strictp elabpath origx)
        (vl-follow-hidexpr-aux-fn
             x
             trace ss strictp elabpath origx-equiv)))
 :rule-classes :congruence)