		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-instmod-find-port-dir

Signature
(vl-lucid-instmod-find-port-dir name inst-ss) → dir
Arguments: name — Guard (stringp name).; inst-ss — Guard (vl-scopestack-p inst-ss).
Returns: dir — Type (vl-maybe-direction-p dir).

Definitions and Theorems

Function: vl-lucid-instmod-find-port-dir

(defun vl-lucid-instmod-find-port-dir (name inst-ss)
  (declare (xargs :guard (and (stringp name)
                              (vl-scopestack-p inst-ss))))
  (let ((__function__ 'vl-lucid-instmod-find-port-dir))
    (declare (ignorable __function__))
    (b* (((unless (vl-scopestack-case inst-ss :local))
          nil)
         (scope (vl-scopestack-local->top inst-ss))
         (portdecl (vl-scope-find-portdecl-fast name scope))
         ((unless portdecl) nil))
      (vl-portdecl->dir portdecl))))

Theorem: vl-maybe-direction-p-of-vl-lucid-instmod-find-port-dir

(defthm vl-maybe-direction-p-of-vl-lucid-instmod-find-port-dir
  (b* ((dir (vl-lucid-instmod-find-port-dir name inst-ss)))
    (vl-maybe-direction-p dir))
  :rule-classes :rewrite)

Theorem: vl-lucid-instmod-find-port-dir-of-str-fix-name

(defthm vl-lucid-instmod-find-port-dir-of-str-fix-name
  (equal (vl-lucid-instmod-find-port-dir (str-fix name)
                                         inst-ss)
         (vl-lucid-instmod-find-port-dir name inst-ss)))

Theorem: vl-lucid-instmod-find-port-dir-streqv-congruence-on-name

(defthm vl-lucid-instmod-find-port-dir-streqv-congruence-on-name
  (implies
       (streqv name name-equiv)
       (equal (vl-lucid-instmod-find-port-dir name inst-ss)
              (vl-lucid-instmod-find-port-dir name-equiv inst-ss)))
  :rule-classes :congruence)

Theorem: vl-lucid-instmod-find-port-dir-of-vl-scopestack-fix-inst-ss

(defthm vl-lucid-instmod-find-port-dir-of-vl-scopestack-fix-inst-ss
 (equal
   (vl-lucid-instmod-find-port-dir name (vl-scopestack-fix inst-ss))
   (vl-lucid-instmod-find-port-dir name inst-ss)))

Theorem: vl-lucid-instmod-find-port-dir-vl-scopestack-equiv-congruence-on-inst-ss

(defthm
 vl-lucid-instmod-find-port-dir-vl-scopestack-equiv-congruence-on-inst-ss
 (implies
      (vl-scopestack-equiv inst-ss inst-ss-equiv)
      (equal (vl-lucid-instmod-find-port-dir name inst-ss)
             (vl-lucid-instmod-find-port-dir name inst-ss-equiv)))
 :rule-classes :congruence)