Core routine for following hierarchical identifiers.
(vl-follow-hidexpr-aux x trace ss &key strictp (origx 'origx) (ctx 'ctx)) → (mv err new-trace tail)
See vl-follow-hidexpr for detailed discussion. This
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)