• Top

• Sv::vl-moddb.lisp

Vl-vardecl-enum-fixup

Signature

(vl-vardecl-enum-fixup x portdecls config) → fixups

Arguments

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

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

Returns

fixups — Type (sv::assigns-p fixups).

Definitions and Theorems

Function: vl-vardecl-enum-fixup

(defun vl-vardecl-enum-fixup (x portdecls config)
  (declare (xargs :guard (and (vl-vardecl-p x)
                              (vl-simpconfig-p config))))
  (declare (xargs :guard
                  (b* (((vl-vardecl x)))
                    (and (vl-datatype-resolved-p x.type)
                         (b* (((mv err size)
                               (vl-datatype-size x.type)))
                           (and (not err) size))))))
  (let ((__function__ 'vl-vardecl-enum-fixup))
    (declare (ignorable __function__))
    (b* (((vl-simpconfig config))
         ((vl-vardecl x))
         (vttree nil)
         ((unless config.enum-fixups) vttree)
         ((unless (or (eq config.enum-fixups :all)
                      (hons-get x.name portdecls)))
          nil)
         ((mv fixups &)
          (vl-datatype-fixup x.type (sv::make-simple-svar x.name)
                             0)))
      fixups)))

Theorem: assigns-p-of-vl-vardecl-enum-fixup

(defthm assigns-p-of-vl-vardecl-enum-fixup
  (b* ((fixups (vl-vardecl-enum-fixup x portdecls config)))
    (sv::assigns-p fixups))
  :rule-classes :rewrite)

Theorem: vars-of-vl-vardecl-enum-fixup

(defthm vars-of-vl-vardecl-enum-fixup
  (b* ((?fixups (vl-vardecl-enum-fixup x portdecls config)))
    (sv::svarlist-addr-p (sv::assigns-vars fixups))))

Theorem: vl-vardecl-enum-fixup-of-vl-vardecl-fix-x

(defthm vl-vardecl-enum-fixup-of-vl-vardecl-fix-x
  (equal (vl-vardecl-enum-fixup (vl-vardecl-fix x)
                                portdecls config)
         (vl-vardecl-enum-fixup x portdecls config)))

Theorem: vl-vardecl-enum-fixup-vl-vardecl-equiv-congruence-on-x

(defthm vl-vardecl-enum-fixup-vl-vardecl-equiv-congruence-on-x
  (implies (vl-vardecl-equiv x x-equiv)
           (equal (vl-vardecl-enum-fixup x portdecls config)
                  (vl-vardecl-enum-fixup x-equiv portdecls config)))
  :rule-classes :congruence)

Theorem: vl-vardecl-enum-fixup-of-vl-simpconfig-fix-config

(defthm vl-vardecl-enum-fixup-of-vl-simpconfig-fix-config
 (equal
      (vl-vardecl-enum-fixup x portdecls (vl-simpconfig-fix config))
      (vl-vardecl-enum-fixup x portdecls config)))

Theorem: vl-vardecl-enum-fixup-vl-simpconfig-equiv-congruence-on-config

(defthm
     vl-vardecl-enum-fixup-vl-simpconfig-equiv-congruence-on-config
  (implies (vl-simpconfig-equiv config config-equiv)
           (equal (vl-vardecl-enum-fixup x portdecls config)
                  (vl-vardecl-enum-fixup x portdecls config-equiv)))
  :rule-classes :congruence)