		Search-engine friendly clone of the ACL2 documentation.

Generate-block-nameclash-items

Vl-scope->raw-generates

Get the raw list of generate statements from any scope.

Signature
(vl-scope->raw-generates x) → generates
Arguments: x — Guard (vl-scope-p x).
Returns: generates — Type (vl-genelementlist-p generates).

Definitions and Theorems

Function: vl-scope->raw-generates

(defun vl-scope->raw-generates (x)
  (declare (xargs :guard (vl-scope-p x)))
  (let ((__function__ 'vl-scope->raw-generates))
    (declare (ignorable __function__))
    (let ((x (vl-scope-fix x)))
      (case (tag x)
            (:vl-interface (vl-interface->generates x))
            (:vl-module (vl-module->generates x))
            (:vl-genblob (vl-genblob->generates x))
            (:vl-blockscope nil)
            (:vl-design nil)
            (:vl-package nil)
            (:vl-class nil)
            (:vl-scopeinfo nil)
            (otherwise (impossible))))))

Theorem: vl-genelementlist-p-of-vl-scope->raw-generates

(defthm vl-genelementlist-p-of-vl-scope->raw-generates
  (b* ((generates (vl-scope->raw-generates x)))
    (vl-genelementlist-p generates))
  :rule-classes :rewrite)

Theorem: vl-scope->raw-generates-of-vl-scope-fix-x

(defthm vl-scope->raw-generates-of-vl-scope-fix-x
  (equal (vl-scope->raw-generates (vl-scope-fix x))
         (vl-scope->raw-generates x)))

Theorem: vl-scope->raw-generates-vl-scope-equiv-congruence-on-x

(defthm vl-scope->raw-generates-vl-scope-equiv-congruence-on-x
  (implies (vl-scope-equiv x x-equiv)
           (equal (vl-scope->raw-generates x)
                  (vl-scope->raw-generates x-equiv)))
  :rule-classes :congruence)