		Search-engine friendly clone of the ACL2 documentation.

Vl-lucidstate-init

Vl-luciddb-init

Construct the initial lucid database for a design.

Signature
(vl-luciddb-init x) → db
Arguments: x — Guard (vl-design-p x).
Returns: db — Type (vl-luciddb-p db).

Definitions and Theorems

Function: vl-luciddb-init

(defun vl-luciddb-init (x)
  (declare (xargs :guard (vl-design-p x)))
  (let ((__function__ 'vl-luciddb-init))
    (declare (ignorable __function__))
    (b* (((vl-design x) (vl-design-fix x))
         (ss (vl-scopestack-init x))
         (db nil)
         (db (vl-scope-luciddb-init x ss db))
         (db (vl-modulelist-luciddb-init x.mods ss db))
         (db (vl-fundecllist-luciddb-init x.fundecls ss db))
         (db (vl-taskdecllist-luciddb-init x.taskdecls ss db))
         (db (vl-packagelist-luciddb-init x.packages ss db))
         (db (vl-interfacelist-luciddb-init x.interfaces ss db)))
      db)))

Theorem: vl-luciddb-p-of-vl-luciddb-init

(defthm vl-luciddb-p-of-vl-luciddb-init
  (b* ((db (vl-luciddb-init x)))
    (vl-luciddb-p db))
  :rule-classes :rewrite)

Theorem: vl-luciddb-init-of-vl-design-fix-x

(defthm vl-luciddb-init-of-vl-design-fix-x
  (equal (vl-luciddb-init (vl-design-fix x))
         (vl-luciddb-init x)))

Theorem: vl-luciddb-init-vl-design-equiv-congruence-on-x

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