• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • 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

• Hid-tools

Vl-follow-hidexpr

Follow a HID to find the associated declaration.

Signature

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

Arguments

x — Hierarchical identifier to follow.
    Guard (vl-hidexpr-p x).

ss — Scopestack where the HID originates.
    Guard (vl-scopestack-p ss).

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

strictp — Require all array indices and bounds to be resolved?.
    Guard (booleanp strictp).

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

Returns

err — A message on any error.
    Type (iff (vl-msg-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).

context — On success, a scopecontext object describing where this hid is rooted.
    Type (implies (not err) (vl-scopecontext-p context)).

tail — On success: the remainder of x after arriving at the declaration. This may include array indexing or structure indexing.
    Type (vl-hidexpr-p tail).

Prerequisite: see hid-tools 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-msg-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 origx strictp elabpath)
 (declare (xargs :guard (and (vl-hidexpr-p x)
                             (vl-scopestack-p ss)
                             (vl-scopeexpr-p origx)
                             (booleanp strictp)
                             (vl-elabtraversal-p elabpath))))
 (let ((__function__ 'vl-follow-hidexpr))
  (declare (ignorable __function__))
  (b*
   ((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))))
    (trace nil)
    ((when (eq name1 :vl-$root))
     (mv (vl-follow-hidexpr-error "$root isn't supported yet" ss)
         trace nil x))
    ((mv item ctx-ss pkg-name)
     (vl-scopestack-find-item/context name1 ss))
    ((when item)
     (b*
      (((mv err trace tail)
        (vl-follow-hidexpr-aux x nil ss
                               :strictp strictp
                               :elabpath elabpath))
       ((when err) (mv err trace nil tail))
       ((mv err context)
        (cond
         (pkg-name
          (b*
           ((pkg (vl-scopestack-find-package pkg-name ss))
            ((unless pkg)
             (mv
              (vmsg
               "Programming error: found item in ~
                                      package ~s0 but couldn't find package"
               pkg-name)
              nil)))
           (mv nil
               (make-vl-scopecontext-package :pkg pkg))))
         ((vl-scopestack-case ctx-ss :global)
          (mv nil (make-vl-scopecontext-root)))
         (t
          (mv
           nil
           (make-vl-scopecontext-local
              :levels (- (vl-scopestack-nesting-level ss)
                         (vl-scopestack-nesting-level ctx-ss))))))))
      (mv err trace context tail)))
    ((when (eq kind :end))
     (mv (vl-follow-hidexpr-error "item not found" ss)
         trace nil x))
    (design (vl-scopestack->design ss))
    ((unless design)
     (mv (vl-follow-hidexpr-error "item not found" ss)
         trace nil x))
    (toplevel (vl-design-toplevel design))
    ((unless (member-equal name1 toplevel))
     (mv (vl-follow-hidexpr-error "item not found" ss)
         trace nil x))
    ((when (consp indices))
     (mv
      (vl-follow-hidexpr-error "array indices into top level module"
                               ss)
      trace nil x))
    (topdef
      (or (vl-find-module name1 (vl-design->mods design))
          (vl-find-interface name1 (vl-design->interfaces design))))
    (topdef-ss (vl-scopestack-init design))
    (next-ss (vl-scopestack-push topdef topdef-ss))
    (elabpath
        (list (vl-elabinstruction-push-named (vl-elabkey-def name1))
              (vl-elabinstruction-root)))
    ((mv err trace tail)
     (vl-follow-hidexpr-aux rest trace next-ss
                            :strictp strictp
                            :elabpath elabpath))
    (context (if (eq (tag topdef) :vl-module)
                 (make-vl-scopecontext-module :mod topdef)
               (make-vl-scopecontext-interface :iface topdef))))
   (mv err trace context tail))))

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

(defthm return-type-of-vl-follow-hidexpr.err
  (b* (((mv ?err
            common-lisp::?trace ?context set::?tail)
        (vl-follow-hidexpr-fn x ss origx strictp elabpath)))
    (iff (vl-msg-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 ?context set::?tail)
        (vl-follow-hidexpr-fn x ss origx strictp elabpath)))
    (vl-hidtrace-p trace))
  :rule-classes :rewrite)

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

(defthm return-type-of-vl-follow-hidexpr.context
  (b* (((mv ?err
            common-lisp::?trace ?context set::?tail)
        (vl-follow-hidexpr-fn x ss origx strictp elabpath)))
    (implies (not err)
             (vl-scopecontext-p context)))
  :rule-classes :rewrite)

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

(defthm vl-hidexpr-p-of-vl-follow-hidexpr.tail
  (b* (((mv ?err
            common-lisp::?trace ?context set::?tail)
        (vl-follow-hidexpr-fn x ss origx strictp elabpath)))
    (vl-hidexpr-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 ?context set::?tail)
        (vl-follow-hidexpr-fn x ss origx strictp elabpath)))
    (implies (not err) (consp trace))))

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

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

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

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

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

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

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

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

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

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

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

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

(defthm vl-follow-hidexpr-fn-vl-scopeexpr-equiv-congruence-on-origx
 (implies
   (vl-scopeexpr-equiv origx origx-equiv)
   (equal (vl-follow-hidexpr-fn x ss origx strictp elabpath)
          (vl-follow-hidexpr-fn x ss origx-equiv strictp elabpath)))
 :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 origx (acl2::bool-fix strictp)
                               elabpath)
         (vl-follow-hidexpr-fn x ss origx strictp elabpath)))

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

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

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

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

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

Subtopics

Vl-follow-hidexpr-aux

Core routine for following hierarchical identifiers.