• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • 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-typedef-enumname-declarations
            • Vl-vardecl-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
  • Testing-utilities
  • Math

• Enum-names

Vl-enumname-range-declarations

For example: given a ranged enum item like foo[3:0], we create the parameters for foo3, foo2, foo1, and foo0.

Signature

(vl-enumname-range-declarations 
     name 
     top bottom nextval basetype atts loc) 
 
  → 
(mv params new-nextval)

Arguments

name — Guard (stringp name).

top — Guard (integerp top).

bottom — Guard (integerp bottom).

nextval — We use an expression, instead of a constant, so that we can support enums where the values being assigned to an enum item depend on other parameters. For example: enum { foo = myparam, bar, baz }.
    Guard (vl-expr-p nextval).

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

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

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

Returns

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

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

Definitions and Theorems

Function: vl-enumname-range-declarations

(defun
 vl-enumname-range-declarations
 (name top bottom nextval basetype atts loc)
 (declare (xargs :guard (and (stringp name)
                             (integerp top)
                             (integerp bottom)
                             (vl-expr-p nextval)
                             (vl-datatype-p basetype)
                             (vl-atts-p atts)
                             (vl-location-p loc))))
 (let
  ((__function__ 'vl-enumname-range-declarations))
  (declare (ignorable __function__))
  (b*
   ((top (lifix top))
    (bottom (lifix bottom))
    (name1 (cat name (if (< top 0) "-" "")
                (natstr (abs top))))
    (first
     (make-vl-paramdecl
         :name name1
         :localp t
         :type
         (make-vl-explicitvalueparam :type basetype
                                     :default (vl-expr-fix nextval))
         :atts atts
         :loc loc))
    (nextval (make-vl-binary :op :vl-binary-plus
                             :left (vl-idexpr name1)
                             :right (vl-make-index 1)))
    ((when (eql top bottom))
     (mv (list first) nextval))
    ((mv decls nextval)
     (vl-enumname-range-declarations
          name
          (if (< top bottom) (1+ top) (1- top))
          bottom nextval basetype atts loc)))
   (mv (cons first decls) nextval))))

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

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

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

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

Theorem: vl-enumname-range-declarations-of-str-fix-name

(defthm vl-enumname-range-declarations-of-str-fix-name
        (equal (vl-enumname-range-declarations
                    (str-fix name)
                    top bottom nextval basetype atts loc)
               (vl-enumname-range-declarations
                    name
                    top bottom nextval basetype atts loc)))

Theorem: vl-enumname-range-declarations-streqv-congruence-on-name

(defthm vl-enumname-range-declarations-streqv-congruence-on-name
        (implies (streqv name name-equiv)
                 (equal (vl-enumname-range-declarations
                             name
                             top bottom nextval basetype atts loc)
                        (vl-enumname-range-declarations
                             name-equiv
                             top bottom nextval basetype atts loc)))
        :rule-classes :congruence)

Theorem: vl-enumname-range-declarations-of-ifix-top

(defthm
 vl-enumname-range-declarations-of-ifix-top
 (equal
   (vl-enumname-range-declarations name (ifix top)
                                   bottom nextval basetype atts loc)
   (vl-enumname-range-declarations
        name
        top bottom nextval basetype atts loc)))

Theorem: vl-enumname-range-declarations-int-equiv-congruence-on-top

(defthm vl-enumname-range-declarations-int-equiv-congruence-on-top
        (implies (acl2::int-equiv top top-equiv)
                 (equal (vl-enumname-range-declarations
                             name
                             top bottom nextval basetype atts loc)
                        (vl-enumname-range-declarations
                             name top-equiv
                             bottom nextval basetype atts loc)))
        :rule-classes :congruence)

Theorem: vl-enumname-range-declarations-of-ifix-bottom

(defthm
   vl-enumname-range-declarations-of-ifix-bottom
   (equal (vl-enumname-range-declarations name top (ifix bottom)
                                          nextval basetype atts loc)
          (vl-enumname-range-declarations
               name
               top bottom nextval basetype atts loc)))

Theorem: vl-enumname-range-declarations-int-equiv-congruence-on-bottom

(defthm
 vl-enumname-range-declarations-int-equiv-congruence-on-bottom
 (implies
   (acl2::int-equiv bottom bottom-equiv)
   (equal
        (vl-enumname-range-declarations
             name
             top bottom nextval basetype atts loc)
        (vl-enumname-range-declarations name top bottom-equiv
                                        nextval basetype atts loc)))
 :rule-classes :congruence)

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

(defthm vl-enumname-range-declarations-of-vl-expr-fix-nextval
        (equal (vl-enumname-range-declarations
                    name top bottom (vl-expr-fix nextval)
                    basetype atts loc)
               (vl-enumname-range-declarations
                    name
                    top bottom nextval basetype atts loc)))

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

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

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

(defthm
 vl-enumname-range-declarations-of-vl-datatype-fix-basetype
 (equal
  (vl-enumname-range-declarations name top bottom
                                  nextval (vl-datatype-fix basetype)
                                  atts loc)
  (vl-enumname-range-declarations
       name
       top bottom nextval basetype atts loc)))

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

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

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

(defthm vl-enumname-range-declarations-of-vl-atts-fix-atts
        (equal (vl-enumname-range-declarations
                    name top bottom
                    nextval basetype (vl-atts-fix atts)
                    loc)
               (vl-enumname-range-declarations
                    name
                    top bottom nextval basetype atts loc)))

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

(defthm
     vl-enumname-range-declarations-vl-atts-equiv-congruence-on-atts
     (implies (vl-atts-equiv atts atts-equiv)
              (equal (vl-enumname-range-declarations
                          name
                          top bottom nextval basetype atts loc)
                     (vl-enumname-range-declarations
                          name top bottom
                          nextval basetype atts-equiv loc)))
     :rule-classes :congruence)

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

(defthm vl-enumname-range-declarations-of-vl-location-fix-loc
        (equal (vl-enumname-range-declarations
                    name top bottom nextval
                    basetype atts (vl-location-fix loc))
               (vl-enumname-range-declarations
                    name
                    top bottom nextval basetype atts loc)))

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

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