		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucidstate-init

Construct the initial lucid state for a design.

Signature
(vl-lucidstate-init x &key (paramsp 't) (generatesp 't)) → st
Arguments: x — Guard (vl-design-p x).; paramsp — Guard (booleanp paramsp).; generatesp — Guard (booleanp generatesp).
Returns: st — Type (vl-lucidstate-p st).

Definitions and Theorems

Function: vl-lucidstate-init-fn

(defun vl-lucidstate-init-fn (x paramsp generatesp)
  (declare (xargs :guard (and (vl-design-p x)
                              (booleanp paramsp)
                              (booleanp generatesp))))
  (let ((__function__ 'vl-lucidstate-init))
    (declare (ignorable __function__))
    (make-vl-lucidstate :db (vl-luciddb-init x)
                        :paramsp paramsp
                        :generatesp generatesp)))

Theorem: vl-lucidstate-p-of-vl-lucidstate-init

(defthm vl-lucidstate-p-of-vl-lucidstate-init
  (b* ((st (vl-lucidstate-init-fn x paramsp generatesp)))
    (vl-lucidstate-p st))
  :rule-classes :rewrite)

Theorem: vl-lucidstate-init-fn-of-vl-design-fix-x

(defthm vl-lucidstate-init-fn-of-vl-design-fix-x
  (equal (vl-lucidstate-init-fn (vl-design-fix x)
                                paramsp generatesp)
         (vl-lucidstate-init-fn x paramsp generatesp)))

Theorem: vl-lucidstate-init-fn-vl-design-equiv-congruence-on-x

(defthm vl-lucidstate-init-fn-vl-design-equiv-congruence-on-x
  (implies
       (vl-design-equiv x x-equiv)
       (equal (vl-lucidstate-init-fn x paramsp generatesp)
              (vl-lucidstate-init-fn x-equiv paramsp generatesp)))
  :rule-classes :congruence)

Theorem: vl-lucidstate-init-fn-of-bool-fix-paramsp

(defthm vl-lucidstate-init-fn-of-bool-fix-paramsp
  (equal (vl-lucidstate-init-fn x (acl2::bool-fix paramsp)
                                generatesp)
         (vl-lucidstate-init-fn x paramsp generatesp)))

Theorem: vl-lucidstate-init-fn-iff-congruence-on-paramsp

(defthm vl-lucidstate-init-fn-iff-congruence-on-paramsp
  (implies
       (iff paramsp paramsp-equiv)
       (equal (vl-lucidstate-init-fn x paramsp generatesp)
              (vl-lucidstate-init-fn x paramsp-equiv generatesp)))
  :rule-classes :congruence)

Theorem: vl-lucidstate-init-fn-of-bool-fix-generatesp

(defthm vl-lucidstate-init-fn-of-bool-fix-generatesp
  (equal
       (vl-lucidstate-init-fn x paramsp (acl2::bool-fix generatesp))
       (vl-lucidstate-init-fn x paramsp generatesp)))

Theorem: vl-lucidstate-init-fn-iff-congruence-on-generatesp

(defthm vl-lucidstate-init-fn-iff-congruence-on-generatesp
  (implies
       (iff generatesp generatesp-equiv)
       (equal (vl-lucidstate-init-fn x paramsp generatesp)
              (vl-lucidstate-init-fn x paramsp generatesp-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-scope-luciddb-init: Initialize variables for a scope.
Vl-taskdecllist-luciddb-init
Vl-interfacelist-luciddb-init
Vl-packagelist-luciddb-init
Vl-modulelist-luciddb-init
Vl-initiallist-luciddb-init
Vl-fundecllist-luciddb-init
Vl-alwayslist-luciddb-init
Vl-taskdecl-luciddb-init
Vl-package-luciddb-init
Vl-interface-luciddb-init
Vl-fundecl-luciddb-init
Vl-module-luciddb-init
Vl-initial-luciddb-init
Vl-always-luciddb-init
Vl-luciddb-init: Construct the initial lucid database for a design.