• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
        • Unparameterization
        • Elaborate
        • Addnames
        • Annotate
          • Increment-elim
          • Make-implicit-wires
          • Basic-bind-elim
          • Argresolve
          • Basicsanity
          • Portdecl-sign
          • Enum-names
            • Vl-enumname-range-declarations
            • Vl-interfacelist-add-enumname-declarations
            • Vl-packagelist-add-enumname-declarations
            • Vl-modulelist-add-enumname-declarations
            • Vl-classlist-add-enumname-declarations
            • Vl-enumitemlist-enumname-declarations
            • Vl-enumname-declarations
            • Vl-paramdecl-enumname-declarations
            • Vl-paramdecllist-enumname-declarations
            • Vl-vardecllist-enumname-declarations
            • Vl-typedeflist-enumname-declarations
            • Vl-vardecl-enumname-declarations
            • Vl-typedef-enumname-declarations
            • Vl-package-add-enumname-declarations
            • Vl-design-add-enumname-declarations
            • Vl-interface-add-enumname-declarations
            • Vl-class-add-enumname-declarations
            • Vl-module-add-enumname-declarations
            • Vl-datatype-map
          • Port-resolve
          • Udp-elim
          • Vl-annotate-design
          • Vl-annotate-module
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Enum-names

Vl-enumname-declarations

Signature

(vl-enumname-declarations x nextval basetype atts loc) 
  → 
(mv warnings params new-nextval)

Arguments

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

nextval — Guard (vl-expr-p nextval).

basetype — Guard (vl-datatype-p basetype).

atts — Guard (vl-atts-p atts).

loc — Guard (vl-location-p loc).

Returns

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

params — Type (vl-paramdecllist-p params).

new-nextval — Type (vl-expr-p new-nextval).

Definitions and Theorems

Function: vl-enumname-declarations

(defun vl-enumname-declarations (x nextval basetype atts loc)
 (declare (xargs :guard (and (vl-enumitem-p x)
                             (vl-expr-p nextval)
                             (vl-datatype-p basetype)
                             (vl-atts-p atts)
                             (vl-location-p loc))))
 (let ((__function__ 'vl-enumname-declarations))
   (declare (ignorable __function__))
   (b*
    (((vl-enumitem x))
     (nextval (vl-expr-fix nextval))
     (warnings nil)
     (val (or x.value nextval))
     ((unless x.range)
      (b*
        ((decl (make-vl-paramdecl
                    :name x.name
                    :localp t
                    :type (make-vl-explicitvalueparam :type basetype
                                                      :default val)
                    :atts atts
                    :loc loc))
         (nextval (make-vl-binary :op :vl-binary-plus
                                  :left (vl-idexpr x.name)
                                  :right (vl-make-index 1))))
        (mv (ok) (list decl) nextval)))
     ((unless (vl-range-resolved-p x.range))
      (mv (warn :type :vl-enum-declarations-fail
                :msg "Non-constant range on enum item ~s0"
                :args (list x.name))
          nil nextval))
     ((vl-range x.range))
     ((mv decls nextval)
      (vl-enumname-range-declarations
           x.name (vl-resolved->val x.range.msb)
           (vl-resolved->val x.range.lsb)
           val basetype atts loc)))
    (mv (ok) decls nextval))))

Theorem: vl-warninglist-p-of-vl-enumname-declarations.warnings

(defthm vl-warninglist-p-of-vl-enumname-declarations.warnings
  (b* (((mv ?warnings ?params ?new-nextval)
        (vl-enumname-declarations x nextval basetype atts loc)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-paramdecllist-p-of-vl-enumname-declarations.params

(defthm vl-paramdecllist-p-of-vl-enumname-declarations.params
  (b* (((mv ?warnings ?params ?new-nextval)
        (vl-enumname-declarations x nextval basetype atts loc)))
    (vl-paramdecllist-p params))
  :rule-classes :rewrite)

Theorem: vl-expr-p-of-vl-enumname-declarations.new-nextval

(defthm vl-expr-p-of-vl-enumname-declarations.new-nextval
  (b* (((mv ?warnings ?params ?new-nextval)
        (vl-enumname-declarations x nextval basetype atts loc)))
    (vl-expr-p new-nextval))
  :rule-classes :rewrite)

Theorem: vl-enumname-declarations-of-vl-enumitem-fix-x

(defthm vl-enumname-declarations-of-vl-enumitem-fix-x
  (equal (vl-enumname-declarations (vl-enumitem-fix x)
                                   nextval basetype atts loc)
         (vl-enumname-declarations x nextval basetype atts loc)))

Theorem: vl-enumname-declarations-vl-enumitem-equiv-congruence-on-x

(defthm vl-enumname-declarations-vl-enumitem-equiv-congruence-on-x
 (implies
  (vl-enumitem-equiv x x-equiv)
  (equal
      (vl-enumname-declarations x nextval basetype atts loc)
      (vl-enumname-declarations x-equiv nextval basetype atts loc)))
 :rule-classes :congruence)

Theorem: vl-enumname-declarations-of-vl-expr-fix-nextval

(defthm vl-enumname-declarations-of-vl-expr-fix-nextval
  (equal (vl-enumname-declarations x (vl-expr-fix nextval)
                                   basetype atts loc)
         (vl-enumname-declarations x nextval basetype atts loc)))

Theorem: vl-enumname-declarations-vl-expr-equiv-congruence-on-nextval

(defthm vl-enumname-declarations-vl-expr-equiv-congruence-on-nextval
 (implies
  (vl-expr-equiv nextval nextval-equiv)
  (equal
      (vl-enumname-declarations x nextval basetype atts loc)
      (vl-enumname-declarations x nextval-equiv basetype atts loc)))
 :rule-classes :congruence)

Theorem: vl-enumname-declarations-of-vl-datatype-fix-basetype

(defthm vl-enumname-declarations-of-vl-datatype-fix-basetype
 (equal
      (vl-enumname-declarations x nextval (vl-datatype-fix basetype)
                                atts loc)
      (vl-enumname-declarations x nextval basetype atts loc)))

Theorem: vl-enumname-declarations-vl-datatype-equiv-congruence-on-basetype

(defthm
  vl-enumname-declarations-vl-datatype-equiv-congruence-on-basetype
 (implies
  (vl-datatype-equiv basetype basetype-equiv)
  (equal
      (vl-enumname-declarations x nextval basetype atts loc)
      (vl-enumname-declarations x nextval basetype-equiv atts loc)))
 :rule-classes :congruence)

Theorem: vl-enumname-declarations-of-vl-atts-fix-atts

(defthm vl-enumname-declarations-of-vl-atts-fix-atts
 (equal
     (vl-enumname-declarations x nextval basetype (vl-atts-fix atts)
                               loc)
     (vl-enumname-declarations x nextval basetype atts loc)))

Theorem: vl-enumname-declarations-vl-atts-equiv-congruence-on-atts

(defthm vl-enumname-declarations-vl-atts-equiv-congruence-on-atts
 (implies
  (vl-atts-equiv atts atts-equiv)
  (equal
      (vl-enumname-declarations x nextval basetype atts loc)
      (vl-enumname-declarations x nextval basetype atts-equiv loc)))
 :rule-classes :congruence)

Theorem: vl-enumname-declarations-of-vl-location-fix-loc

(defthm vl-enumname-declarations-of-vl-location-fix-loc
 (equal
      (vl-enumname-declarations x nextval
                                basetype atts (vl-location-fix loc))
      (vl-enumname-declarations x nextval basetype atts loc)))

Theorem: vl-enumname-declarations-vl-location-equiv-congruence-on-loc

(defthm vl-enumname-declarations-vl-location-equiv-congruence-on-loc
 (implies
  (vl-location-equiv loc loc-equiv)
  (equal
      (vl-enumname-declarations x nextval basetype atts loc)
      (vl-enumname-declarations x nextval basetype atts loc-equiv)))
 :rule-classes :congruence)