• Top

• Sv::vl-moddb.lisp

Vl-modulelist->svex-modalist

Signature

(vl-modulelist->svex-modalist x elabindex config modalist) 
  → 
(mv warnings modalist1 new-elabindex)

Arguments

x — Guard (vl-modulelist-p x).

elabindex — global scope.

config — Guard (vl-simpconfig-p config).

modalist — Guard (sv::modalist-p modalist).

Returns

warnings — Type (vl-reportcard-p warnings).

modalist1 — Type (and (sv::modalist-p modalist1) (implies (sv::svarlist-addr-p (sv::modalist-vars modalist)) (sv::svarlist-addr-p (sv::modalist-vars modalist1)))) .

Definitions and Theorems

Function: vl-modulelist->svex-modalist

(defun vl-modulelist->svex-modalist (x elabindex config modalist)
 (declare (xargs :stobjs (elabindex)))
 (declare (xargs :guard (and (vl-modulelist-p x)
                             (vl-simpconfig-p config)
                             (sv::modalist-p modalist))))
 (let ((__function__ 'vl-modulelist->svex-modalist))
   (declare (ignorable __function__))
   (b*
    (((when (atom x))
      (mv nil (sv::modalist-fix modalist)
          elabindex))
     (name (vl-module->name (car x)))
     ((mv warnings modalist elabindex)
      (time$ (vl-module->svex-module name elabindex config modalist)
             :msg "; mod->sv ~s0: ~st sec, ~sa bytes~%"
             :args (list name)
             :mintime 1))
     ((mv reportcard modalist elabindex)
      (vl-modulelist->svex-modalist (cdr x)
                                    elabindex config modalist)))
    (mv (if warnings (cons (cons name warnings) reportcard)
          reportcard)
        modalist elabindex))))

Theorem: vl-reportcard-p-of-vl-modulelist->svex-modalist.warnings

(defthm vl-reportcard-p-of-vl-modulelist->svex-modalist.warnings
  (b* (((mv ?warnings ?modalist1 ?new-elabindex)
        (vl-modulelist->svex-modalist x elabindex config modalist)))
    (vl-reportcard-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-modulelist->svex-modalist.modalist1

(defthm return-type-of-vl-modulelist->svex-modalist.modalist1
 (b* (((mv ?warnings ?modalist1 ?new-elabindex)
       (vl-modulelist->svex-modalist x elabindex config modalist)))
  (and
     (sv::modalist-p modalist1)
     (implies (sv::svarlist-addr-p (sv::modalist-vars modalist))
              (sv::svarlist-addr-p (sv::modalist-vars modalist1)))))
 :rule-classes :rewrite)

Theorem: vl-modulelist->svex-modalist-of-vl-modulelist-fix-x

(defthm vl-modulelist->svex-modalist-of-vl-modulelist-fix-x
 (equal (vl-modulelist->svex-modalist (vl-modulelist-fix x)
                                      elabindex config modalist)
        (vl-modulelist->svex-modalist x elabindex config modalist)))

Theorem: vl-modulelist->svex-modalist-vl-modulelist-equiv-congruence-on-x

(defthm
   vl-modulelist->svex-modalist-vl-modulelist-equiv-congruence-on-x
 (implies
   (vl-modulelist-equiv x x-equiv)
   (equal (vl-modulelist->svex-modalist x elabindex config modalist)
          (vl-modulelist->svex-modalist
               x-equiv elabindex config modalist)))
 :rule-classes :congruence)

Theorem: vl-modulelist->svex-modalist-of-vl-simpconfig-fix-config

(defthm vl-modulelist->svex-modalist-of-vl-simpconfig-fix-config
 (equal (vl-modulelist->svex-modalist
             x elabindex (vl-simpconfig-fix config)
             modalist)
        (vl-modulelist->svex-modalist x elabindex config modalist)))

Theorem: vl-modulelist->svex-modalist-vl-simpconfig-equiv-congruence-on-config

(defthm
 vl-modulelist->svex-modalist-vl-simpconfig-equiv-congruence-on-config
 (implies
   (vl-simpconfig-equiv config config-equiv)
   (equal (vl-modulelist->svex-modalist x elabindex config modalist)
          (vl-modulelist->svex-modalist
               x elabindex config-equiv modalist)))
 :rule-classes :congruence)

Theorem: vl-modulelist->svex-modalist-of-modalist-fix-modalist

(defthm vl-modulelist->svex-modalist-of-modalist-fix-modalist
 (equal
   (vl-modulelist->svex-modalist x elabindex
                                 config (sv::modalist-fix modalist))
   (vl-modulelist->svex-modalist x elabindex config modalist)))

Theorem: vl-modulelist->svex-modalist-modalist-equiv-congruence-on-modalist

(defthm
 vl-modulelist->svex-modalist-modalist-equiv-congruence-on-modalist
 (implies
   (sv::modalist-equiv modalist modalist-equiv)
   (equal (vl-modulelist->svex-modalist x elabindex config modalist)
          (vl-modulelist->svex-modalist
               x elabindex config modalist-equiv)))
 :rule-classes :congruence)

Subtopics

Sv::vl-moddb.lisp