		Search-engine friendly clone of the ACL2 documentation.

Syntax

Vl-modelement->loc

Signature
(vl-modelement->loc x) → loc
Arguments: x — Guard (vl-modelement-p x).
Returns: loc — Type (vl-location-p loc).

Definitions and Theorems

Function: vl-modelement->loc

(defun vl-modelement->loc (x)
  (declare (xargs :guard (vl-modelement-p x)))
  (let ((__function__ 'vl-modelement->loc))
    (declare (ignorable __function__))
    (let ((x (vl-modelement-fix x)))
      (case (tag x)
            (:vl-portdecl (vl-portdecl->loc x))
            (:vl-assign (vl-assign->loc x))
            (:vl-alias (vl-alias->loc x))
            (:vl-vardecl (vl-vardecl->loc x))
            (:vl-paramdecl (vl-paramdecl->loc x))
            (:vl-fundecl (vl-fundecl->loc x))
            (:vl-taskdecl (vl-taskdecl->loc x))
            (:vl-modinst (vl-modinst->loc x))
            (:vl-gateinst (vl-gateinst->loc x))
            (:vl-always (vl-always->loc x))
            (:vl-initial (vl-initial->loc x))
            (:vl-typedef (vl-typedef->loc x))
            (:vl-import (vl-import->loc x))
            (:vl-fwdtypedef (vl-fwdtypedef->loc x))
            (:vl-modport (vl-modport->loc x))
            (:vl-genvar (vl-genvar->loc x))))))

Theorem: vl-location-p-of-vl-modelement->loc

(defthm vl-location-p-of-vl-modelement->loc
  (b* ((loc (vl-modelement->loc x)))
    (vl-location-p loc))
  :rule-classes :rewrite)

Theorem: vl-modelement->loc-of-vl-modelement-fix-x

(defthm vl-modelement->loc-of-vl-modelement-fix-x
  (equal (vl-modelement->loc (vl-modelement-fix x))
         (vl-modelement->loc x)))

Theorem: vl-modelement->loc-vl-modelement-equiv-congruence-on-x

(defthm vl-modelement->loc-vl-modelement-equiv-congruence-on-x
  (implies (vl-modelement-equiv x x-equiv)
           (equal (vl-modelement->loc x)
                  (vl-modelement->loc x-equiv)))
  :rule-classes :congruence)