• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
          • Following-hids
            • Vl-follow-hidexpr
              • Vl-follow-hidexpr-aux
            • Vl-partselect-type-top-dimension-replacement
            • Vl-hidindex-datatype-resolve-dims
            • Vl-follow-hidexpr-error
            • Vl-follow-hidexpr-dimscheck
            • Vl-index-find-type
            • Vl-follow-hidexpr-dimcheck
            • Vl-partselect-expr-type
            • Vl-ss-find-hidexpr-range!!
            • Vl-hidstep
            • Vl-ss-find-hidexpr-range
            • Vl-genarrayblocklist-find-block
            • Vl-flatten-hidindex
            • Vl-hidexpr-resolved-p
            • Vl-flatten-hidexpr
            • Vl-hidindex-resolved-p
            • Vl-hidtrace
          • Vl-hidexpr-traverse-datatype
          • Abstract-hids
          • Vl-hidexpr-find-type
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • 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 (origx 'origx) 
                       (ctx 'ctx)) 
 
  → 
(mv err new-trace tail)

Arguments

x — HID expression fragment that we are following.
    Guard (vl-expr-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).

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

ctx — Original context, for better error messages.
    Guard (acl2::any-p ctx).

Returns

err — A vl-warning-p on any error.
    Type (iff (vl-warning-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-expr-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 origx ctx)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-hidtrace-p trace)
                             (vl-scopestack-p ss)
                             (booleanp strictp)
                             (vl-expr-p origx)
                             (acl2::any-p ctx))))
 (declare (xargs :guard (vl-hidexpr-p x)))
 (let ((__function__ 'vl-follow-hidexpr-aux))
  (declare (ignorable __function__))
  (b*
   ((trace (vl-hidtrace-fix trace))
    (x (vl-expr-fix x))
    (idx1 (vl-hidexpr->first x))
    (name1 (vl-hidindex->name idx1))
    ((mv item item-ss)
     (vl-scopestack-find-item/ss name1 ss))
    ((unless item)
     (mv (vl-follow-hidexpr-error "item not found" ss)
         trace x))
    (trace (cons (make-vl-hidstep :item item :ss item-ss)
                 trace))
    ((when (or (eq (tag item) :vl-vardecl)
               (eq (tag item) :vl-paramdecl)))
     (mv nil trace x))
    ((when (or (eq (tag item) :vl-fundecl)
               (eq (tag item) :vl-taskdecl)))
     (if (vl-hidexpr->endp x)
         (mv nil trace x)
       (mv (vl-follow-hidexpr-error
                (if (eq (tag item) :vl-fundecl)
                    "hierarchical reference into function"
                  "hierarchical reference into task")
                item-ss)
           trace x)))
    ((when (eq (tag item) :vl-modinst))
     (b* (((vl-modinst item))
          (indices (vl-hidindex->indices idx1))
          (dims (and item.range (list item.range)))
          (err (vl-follow-hidexpr-dimscheck name1 indices dims
                                            :strictp strictp))
          ((when err)
           (mv (vl-follow-hidexpr-error err item-ss)
               trace x))
          ((when (vl-hidexpr->endp x))
           (mv nil trace x))
          ((mv mod mod-ss)
           (vl-scopestack-find-definition/ss item.modname item-ss))
          ((unless mod)
           (mv (vl-follow-hidexpr-error
                    (cat "reference through missing module "
                         item.modname)
                    item-ss)
               trace x))
          (modtag (tag mod))
          ((when (eq modtag :vl-udp))
           (mv (vl-follow-hidexpr-error
                    (cat "reference through primitive "
                         item.modname)
                    item-ss)
               trace x))
          ((unless (or (eq modtag :vl-module)
                       (eq modtag :vl-interface)))
           (mv (vl-follow-hidexpr-error
                    (cat "module instance " name1
                         " of " item.modname ": invalid type "
                         (if (symbolp modtag)
                             (symbol-name modtag)
                           "???"))
                    item-ss)
               trace x))
          (next-ss (vl-scopestack-push mod mod-ss)))
       (vl-follow-hidexpr-aux (vl-hidexpr->rest x)
                              trace next-ss
                              :strictp strictp)))
    ((when (eq (tag item) :vl-interfaceport))
     (b* (((vl-interfaceport item))
          (indices (vl-hidindex->indices idx1))
          ((when (or (consp indices) (consp item.udims)))
           (mv (vl-follow-hidexpr-error
                    "BOZO implement support for interface arrays."
                    item-ss)
               trace x))
          ((when (vl-hidexpr->endp x))
           (mv nil trace x))
          ((mv iface iface-ss)
           (vl-scopestack-find-definition/ss item.ifname item-ss))
          ((unless iface)
           (mv (vl-follow-hidexpr-error
                    (cat "reference through missing interface "
                         item.ifname)
                    item-ss)
               trace x))
          (iftag (tag iface))
          ((unless (eq iftag :vl-interface))
           (mv (vl-follow-hidexpr-error
                    (cat "interface port " name1 " of interface "
                         item.ifname ": invalid type "
                         (if (symbolp iftag)
                             (symbol-name iftag)
                           "???"))
                    item-ss)
               trace x))
          (next-ss (vl-scopestack-push iface iface-ss)))
       (vl-follow-hidexpr-aux (vl-hidexpr->rest x)
                              trace next-ss
                              :strictp strictp)))
    ((when (eq (tag item) :vl-genblock))
     (b* ((indices (vl-hidindex->indices idx1))
          ((when (consp indices))
           (mv (vl-follow-hidexpr-error
                    "array indices on reference to generate block"
                    item-ss)
               trace x))
          ((when (vl-hidexpr->endp x))
           (mv (vl-follow-hidexpr-error
                    "reference to generate block" item-ss)
               trace x))
          (genblob (vl-sort-genelements (vl-genblock->elems item)))
          (next-ss (vl-scopestack-push genblob item-ss)))
       (vl-follow-hidexpr-aux (vl-hidexpr->rest x)
                              trace next-ss
                              :strictp strictp)))
    ((when (eq (tag item) :vl-genarray))
     (b*
      (((when (vl-hidexpr->endp x))
        (mv (vl-follow-hidexpr-error
                 "reference to generate array" item-ss)
            trace x))
       (indices (vl-hidindex->indices idx1))
       ((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-genarrayblocklist-find-block
                   blocknum (vl-genarray->blocks item)))
       ((unless block)
        (mv (vl-follow-hidexpr-error
                 (cat "invalid index into generate array: "
                      (natstr blocknum))
                 item-ss)
            trace x))
       (genblob
            (vl-sort-genelements (vl-genarrayblock->elems block)))
       (next-ss (vl-scopestack-push genblob item-ss)))
      (vl-follow-hidexpr-aux (vl-hidexpr->rest x)
                             trace next-ss
                             :strictp strictp)))
    ((when (eq (tag item) :vl-typedef))
     (mv
        (vl-follow-hidexpr-error "hierarchical reference to typedef"
                                 item-ss)
        trace x))
    ((when (eq (tag item) :vl-modport))
     (mv
       (vl-follow-hidexpr-error "hierarchical reference to modports"
                                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 (cat "hierarchical reference to "
                                       (symbol-name (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 origx ctx)))
    (iff (vl-warning-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 origx ctx)))
    (vl-hidtrace-p new-trace))
  :rule-classes :rewrite)

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

(defthm vl-expr-p-of-vl-follow-hidexpr-aux.tail
  (b* (((mv ?err ?new-trace set::?tail)
        (vl-follow-hidexpr-aux-fn x trace ss strictp origx ctx)))
    (vl-expr-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 origx ctx)))
    (implies (or (consp trace) (not err))
             (consp 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
 (implies
     (vl-hidexpr-p x)
     (b* (((mv ?err ?new-trace set::?tail)
           (vl-follow-hidexpr-aux-fn x trace ss strictp origx ctx)))
       (vl-hidexpr-p tail)))
 :rule-classes :rewrite)

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

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

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

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

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

(defthm vl-follow-hidexpr-aux-fn-vl-expr-equiv-congruence-on-x
 (implies
  (vl-expr-equiv x x-equiv)
  (equal
     (vl-follow-hidexpr-aux-fn x trace ss strictp origx ctx)
     (vl-follow-hidexpr-aux-fn x-equiv trace ss strictp origx ctx)))
 :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 origx ctx)
         (vl-follow-hidexpr-aux-fn x trace ss strictp origx ctx)))

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 origx ctx)
     (vl-follow-hidexpr-aux-fn x trace-equiv ss strictp origx ctx)))
 :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 origx ctx)
         (vl-follow-hidexpr-aux-fn x trace ss strictp origx ctx)))

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 origx ctx)
     (vl-follow-hidexpr-aux-fn x trace ss-equiv strictp origx ctx)))
 :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)
                                 origx ctx)
       (vl-follow-hidexpr-aux-fn x trace ss strictp origx ctx)))

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 origx ctx)
     (vl-follow-hidexpr-aux-fn x trace ss strictp-equiv origx ctx)))
 :rule-classes :congruence)

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

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

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

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

Theorem: vl-follow-hidexpr-aux-fn-of-identity-ctx

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

Theorem: vl-follow-hidexpr-aux-fn-equal-congruence-on-ctx

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