		Search-engine friendly clone of the ACL2 documentation.

Following-hids

Vl-follow-hidexpr

Follow a HID to find the associated declaration.

Signature
(vl-follow-hidexpr x ss ctx &key strictp) → (mv err trace tail)
Arguments: x — Hierarchical identifier to follow.
Guard (vl-expr-p x).; ss — Scopestack where the HID originates.
Guard (vl-scopestack-p ss).; ctx — Context for better error messages.
Guard (acl2::any-p ctx).; strictp — Require all array indices and bounds to be resolved?.
Guard (booleanp strictp).
Returns: err — A warning on any error.
Type (iff (vl-warning-p err) err).; trace — On success: a non-empty trace that records all the items we went through to resolve this HID. The car of the trace is the final declaration for this HID.
Type (vl-hidtrace-p trace).; tail — On success: the remainder of x after arriving at the declaration. This may include array indexing or structure indexing.
Type (vl-expr-p tail).

Prerequisite: see following-hids for considerable discussion about the goals and design of this function.

This is our top-level routine for following hierarchical identifiers. It understands how to resolve both top-level hierarchical identifiers like topmodule.foo.bar and downward identifiers like submodname.foo.bar.

We try to follow x, which must be a proper vl-hidexpr-p, to whatever vl-scopeitem it refers to. This can fail for many reasons, e.g., any piece of x might refer to a name that doesn't exist, might have inappropriate array indices, etc. In case of failure, err is a good vl-warning-p and the other results are not sensible and should not be relied on.

Trace

We return a vl-hidtrace-p that records, in ``backwards'' order, the steps that we took to resolve x. That is: if we are resolving foo.bar.baz, then the first step in the trace will be the declaration for baz, and the last step in the trace will be the lookup for foo. In other words, the first step in the trace corresponds to the ``final'' declaration that x refers to. Many applications won't care about the rest of the trace beyond its first step. However, the rest of the trace may be useful if you are trying to deal with, e.g., all of the interfaces along the hierarchical identifier.

Tail

The trace we return stops at variable declarations. This may be confusing because, in Verilog, the same . syntax is used to index through the module hierarchy and to index through structures. To make this concrete, suppose we have something like:

typedef struct { logic fastMode; ...; } opcode_t;
typedef struct { opcode_t opcode; ... } instruction_t;

module bar (...) ;
  instruction_t instruction1;
  ...
endmodule

module foo (...) ;
  bar mybar(...) ;
  ...
endmodule

module main (...) ;
  foo myfoo(...) ;
  ...
  $display("fastMode is %b", myfoo.mybar.instruction1.opcode.fastMode);
endmodule

When we follow myfoo.mybar.instruction1.opcode.fastMode, our trace will only go to instruction1, because the .opcode.fastMode part is structure indexing, not scope indexing.

To account for this, we return not only the trace but also the tail of the hierarchical identifier that remains where we stop. For instance, in this case the tail would be instruction1.opcode.fastMode.

Definitions and Theorems

Function: vl-follow-hidexpr-fn

(defun vl-follow-hidexpr-fn (x ss ctx strictp)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-scopestack-p ss)
                             (acl2::any-p ctx)
                             (booleanp strictp))))
 (declare (xargs :guard (vl-hidexpr-p x)))
 (let ((__function__ 'vl-follow-hidexpr))
  (declare (ignorable __function__))
  (b*
   ((x (vl-expr-fix x))
    (idx1 (vl-hidexpr->first x))
    (name1 (vl-hidindex->name idx1))
    (origx x)
    (trace nil)
    ((mv item &)
     (vl-scopestack-find-item/ss name1 ss))
    ((when item)
     (vl-follow-hidexpr-aux x nil ss
                            :strictp strictp
                            :ctx ctx))
    ((when (vl-hidexpr->endp x))
     (mv (vl-follow-hidexpr-error "item not found" ss)
         trace x))
    (design (vl-scopestack->design ss))
    ((unless design)
     (mv (vl-follow-hidexpr-error "item not found" ss)
         trace x))
    (mods (vl-design->mods design))
    (toplevel (vl-modulelist-toplevel mods))
    ((unless (member-equal name1 toplevel))
     (mv (vl-follow-hidexpr-error "item not found" ss)
         trace x))
    (indices (vl-hidindex->indices idx1))
    ((when (consp indices))
     (mv
      (vl-follow-hidexpr-error "array indices into top level module"
                               ss)
      trace x))
    (mod (vl-find-module name1 mods))
    (mod-ss (vl-scopestack-init design))
    (next-ss (vl-scopestack-push mod mod-ss)))
   (vl-follow-hidexpr-aux (vl-hidexpr->rest x)
                          trace next-ss
                          :strictp strictp
                          :ctx ctx))))

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

(defthm return-type-of-vl-follow-hidexpr.err
  (b* (((mv ?err common-lisp::?trace set::?tail)
        (vl-follow-hidexpr-fn x ss ctx strictp)))
    (iff (vl-warning-p err) err))
  :rule-classes :rewrite)

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

(defthm vl-hidtrace-p-of-vl-follow-hidexpr.trace
  (b* (((mv ?err common-lisp::?trace set::?tail)
        (vl-follow-hidexpr-fn x ss ctx strictp)))
    (vl-hidtrace-p trace))
  :rule-classes :rewrite)

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

(defthm vl-expr-p-of-vl-follow-hidexpr.tail
  (b* (((mv ?err common-lisp::?trace set::?tail)
        (vl-follow-hidexpr-fn x ss ctx strictp)))
    (vl-expr-p tail))
  :rule-classes :rewrite)

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

(defthm consp-of-vl-follow-hidexpr.trace
  (b* (((mv ?err common-lisp::?trace set::?tail)
        (vl-follow-hidexpr-fn x ss ctx strictp)))
    (implies (not err) (consp trace)))
  :rule-classes :rewrite)

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

(defthm vl-hidexpr-p-of-vl-follow-hidexpr.tail
  (implies (vl-hidexpr-p x)
           (b* (((mv ?err common-lisp::?trace set::?tail)
                 (vl-follow-hidexpr-fn x ss ctx strictp)))
             (vl-hidexpr-p tail)))
  :rule-classes :rewrite)

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

(defthm context-irrelevance-of-vl-follow-hidexpr
  (implies (syntaxp (not (equal ctx (list 'quote nil))))
           (b* (((mv err1 trace1 tail1)
                 (vl-follow-hidexpr x ss ctx
                                    :strictp strictp))
                ((mv err2 trace2 tail2)
                 (vl-follow-hidexpr x ss nil
                                    :strictp strictp)))
             (and (equal trace1 trace2)
                  (equal tail1 tail2)
                  (iff err1 err2)))))

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

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

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

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

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

(defthm vl-follow-hidexpr-fn-of-vl-scopestack-fix-ss
  (equal (vl-follow-hidexpr-fn x (vl-scopestack-fix ss)
                               ctx strictp)
         (vl-follow-hidexpr-fn x ss ctx strictp)))

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

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

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

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

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

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

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

(defthm vl-follow-hidexpr-fn-of-bool-fix-strictp
  (equal (vl-follow-hidexpr-fn x ss ctx (acl2::bool-fix strictp))
         (vl-follow-hidexpr-fn x ss ctx strictp)))

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

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

Subtopics

Vl-follow-hidexpr-aux: Core routine for following hierarchical identifiers.