		Search-engine friendly clone of the ACL2 documentation.

Scopestack

Vl-scopestack-init

Create an initial scope stack for an entire design.

Signature
(vl-scopestack-init design) → ss
Arguments: design — Guard (vl-design-p design).
Returns: ss — Type (vl-scopestack-p ss).

Definitions and Theorems

Function: vl-scopestack-init

(defun vl-scopestack-init (design)
  (declare (xargs :guard (vl-design-p design)))
  (let ((__function__ 'vl-scopestack-init))
    (declare (ignorable __function__))
    (make-vl-scopestack-global :design design)))

Theorem: vl-scopestack-p-of-vl-scopestack-init

(defthm vl-scopestack-p-of-vl-scopestack-init
  (b* ((ss (vl-scopestack-init design)))
    (vl-scopestack-p ss))
  :rule-classes :rewrite)

Theorem: vl-scopestack-init-of-vl-design-fix-design

(defthm vl-scopestack-init-of-vl-design-fix-design
  (equal (vl-scopestack-init (vl-design-fix design))
         (vl-scopestack-init design)))

Theorem: vl-scopestack-init-vl-design-equiv-congruence-on-design

(defthm vl-scopestack-init-vl-design-equiv-congruence-on-design
  (implies (vl-design-equiv design design-equiv)
           (equal (vl-scopestack-init design)
                  (vl-scopestack-init design-equiv)))
  :rule-classes :congruence)