		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-design-lucid

Signature
(vl-design-lucid x &key (modportsp 't) (paramsp 't) (generatesp 't) (typosp 't)) → new-x
Arguments: x — Guard (vl-design-p x).; modportsp — Guard (booleanp modportsp).; paramsp — Guard (booleanp paramsp).; generatesp — Guard (booleanp generatesp).; typosp — Guard (booleanp typosp).
Returns: new-x — Type (vl-design-p new-x).

Definitions and Theorems

Function: vl-design-lucid-fn

(defun vl-design-lucid-fn (x modportsp paramsp generatesp typosp)
 (declare (xargs :guard (and (vl-design-p x)
                             (booleanp modportsp)
                             (booleanp paramsp)
                             (booleanp generatesp)
                             (booleanp typosp))))
 (let ((__function__ 'vl-design-lucid))
  (declare (ignorable __function__))
  (b*
   ((x (cwtime (hons-copy (vl-design-fix x))
               :name vl-design-lucid-hons
               :mintime 1))
    (ss (vl-scopestack-init x))
    (st (cwtime (vl-lucidstate-init x
                                    :modportsp modportsp
                                    :paramsp paramsp
                                    :generatesp generatesp)))
    (st (cwtime (vl-design-lucidcheck-main x ss st)))
    ((mv reportcard typo-candidates)
     (cwtime (vl-lucid-dissect st)))
    (reportcard
     (b*
       (((unless typosp) reportcard)
        (typo-candidates
             (fast-alist-free (fast-alist-clean typo-candidates))))
       (cwtime (vl-lucid-typo-detect typo-candidates reportcard)))))
   (clear-memoize-table 'vl-scopestack->flat-transitive-names-slow)
   (vl-scopestacks-free)
   (vl-apply-reportcard x reportcard))))

Theorem: vl-design-p-of-vl-design-lucid

(defthm vl-design-p-of-vl-design-lucid
 (b*
  ((new-x
        (vl-design-lucid-fn x modportsp paramsp generatesp typosp)))
  (vl-design-p new-x))
 :rule-classes :rewrite)

Theorem: vl-design-lucid-fn-of-vl-design-fix-x

(defthm vl-design-lucid-fn-of-vl-design-fix-x
 (equal (vl-design-lucid-fn (vl-design-fix x)
                            modportsp paramsp generatesp typosp)
        (vl-design-lucid-fn x modportsp paramsp generatesp typosp)))

Theorem: vl-design-lucid-fn-vl-design-equiv-congruence-on-x

(defthm vl-design-lucid-fn-vl-design-equiv-congruence-on-x
 (implies
   (vl-design-equiv x x-equiv)
   (equal (vl-design-lucid-fn x modportsp paramsp generatesp typosp)
          (vl-design-lucid-fn x-equiv
                              modportsp paramsp generatesp typosp)))
 :rule-classes :congruence)

Theorem: vl-design-lucid-fn-of-bool-fix-modportsp

(defthm vl-design-lucid-fn-of-bool-fix-modportsp
 (equal (vl-design-lucid-fn x (acl2::bool-fix modportsp)
                            paramsp generatesp typosp)
        (vl-design-lucid-fn x modportsp paramsp generatesp typosp)))

Theorem: vl-design-lucid-fn-iff-congruence-on-modportsp

(defthm vl-design-lucid-fn-iff-congruence-on-modportsp
 (implies
   (iff modportsp modportsp-equiv)
   (equal (vl-design-lucid-fn x modportsp paramsp generatesp typosp)
          (vl-design-lucid-fn x modportsp-equiv
                              paramsp generatesp typosp)))
 :rule-classes :congruence)

Theorem: vl-design-lucid-fn-of-bool-fix-paramsp

(defthm vl-design-lucid-fn-of-bool-fix-paramsp
 (equal (vl-design-lucid-fn x modportsp (acl2::bool-fix paramsp)
                            generatesp typosp)
        (vl-design-lucid-fn x modportsp paramsp generatesp typosp)))

Theorem: vl-design-lucid-fn-iff-congruence-on-paramsp

(defthm vl-design-lucid-fn-iff-congruence-on-paramsp
 (implies
   (iff paramsp paramsp-equiv)
   (equal (vl-design-lucid-fn x modportsp paramsp generatesp typosp)
          (vl-design-lucid-fn x modportsp
                              paramsp-equiv generatesp typosp)))
 :rule-classes :congruence)

Theorem: vl-design-lucid-fn-of-bool-fix-generatesp

(defthm vl-design-lucid-fn-of-bool-fix-generatesp
 (equal (vl-design-lucid-fn x modportsp
                            paramsp (acl2::bool-fix generatesp)
                            typosp)
        (vl-design-lucid-fn x modportsp paramsp generatesp typosp)))

Theorem: vl-design-lucid-fn-iff-congruence-on-generatesp

(defthm vl-design-lucid-fn-iff-congruence-on-generatesp
 (implies
   (iff generatesp generatesp-equiv)
   (equal (vl-design-lucid-fn x modportsp paramsp generatesp typosp)
          (vl-design-lucid-fn x modportsp
                              paramsp generatesp-equiv typosp)))
 :rule-classes :congruence)

Theorem: vl-design-lucid-fn-of-bool-fix-typosp

(defthm vl-design-lucid-fn-of-bool-fix-typosp
 (equal (vl-design-lucid-fn x modportsp paramsp
                            generatesp (acl2::bool-fix typosp))
        (vl-design-lucid-fn x modportsp paramsp generatesp typosp)))

Theorem: vl-design-lucid-fn-iff-congruence-on-typosp

(defthm vl-design-lucid-fn-iff-congruence-on-typosp
 (implies
   (iff typosp typosp-equiv)
   (equal (vl-design-lucid-fn x modportsp paramsp generatesp typosp)
          (vl-design-lucid-fn x modportsp
                              paramsp generatesp typosp-equiv)))
 :rule-classes :congruence)