• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
        • Symbolic-test-vectors
        • Esim-primitives
        • E-conversion
          • Vl-ealist-p
          • Modinsts-to-eoccs
          • Vl-module-make-esim
          • Exploding-vectors
            • Vl-wirealist-p
            • Emodwire-encoding
            • Vl-emodwire-p
              • Vl-emodwire
              • Vl-emodwirelist-highest
              • Vl-emodwire-fix
              • Vl-emodwire->index
                • Vl-emodwire->basename
              • Vl-emodwirelistlist
              • Vl-emodwirelist
            • Resolving-multiple-drivers
            • Vl-modulelist-make-esims
            • Vl-module-check-e-ok
            • Vl-collect-design-wires
            • Adding-z-drivers
            • Vl-design-to-e
            • Vl-design-to-e-check-ports
            • Vl-design-to-e-main
            • Port-bit-checking
          • Esim-steps
          • Patterns
          • Mod-internal-paths
          • Defmodules
          • Esim-simplify-update-fns
          • Esim-tutorial
          • Esim-vl
        • Vl2014
        • Sv
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-emodwire-p

    Vl-emodwire->index

    Return the index of an vl-emodwire-p as a natural, or nil if there is no index.

    For instance, the index of |opcode[3]| is 3, and the index of |reset| is nil.

    Definitions and Theorems

    Function: vl-emodwire->index

    (defun vl-emodwire->index (x)
      (declare (xargs :guard (vl-emodwire-p x)))
      (and (mbt (vl-emodwire-p x))
           (b* ((name (symbol-name x))
                (open (position #\[ name))
                ((when (not open)) nil)
                (close (position #\] name))
                (index-str (subseq name (+ open 1) close))
                ((mv index-val ?len)
                 (str::parse-nat-from-string
                      index-str 0 0 0 (length index-str))))
             index-val)))

    Theorem: type-of-vl-emodwire->index

    (defthm type-of-vl-emodwire->index
      (or (not (vl-emodwire->index x))
          (natp (vl-emodwire->index x)))
      :rule-classes :type-prescription)

    Theorem: vl-emodwire->index-of-vl-emodwire

    (defthm vl-emodwire->index-of-vl-emodwire
      (implies (and (force (stringp basename))
                    (force (maybe-natp index))
                    (force (or index (not (equal basename "NIL")))))
               (equal (vl-emodwire->index (vl-emodwire basename index))
                      index)))