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