• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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

Construct an emod wire from a base name and index.

No restrictions are placed on the base name because we will automatically encode it if necessary; see emodwire-encoding.

We take special measures to optimize this function: we pre-generate strings "[0]", "[1]", ..., "[255]" so that for indicies under 256 we can avoid some concatenations. This appears to reduce memory usage by about half and reduces run-time by about 30% for a simple loop that builds the wire name foo[33] millions of times, but this timing is based on the fast-cat book and may change if CCL gets a compiler-macro for CONCATENATE.

Note that we emulate defaggregate and add make-vl-emodwire and change-vl-emodwire macros.

Definitions and Theorems

Function: vl-make-indexed-wire-names-array

(defun vl-make-indexed-wire-names-array (n)
  (cons (cons n (cat "[" (natstr n) "]"))
        (if (zp n)
            nil
          (vl-make-indexed-wire-names-array (1- n)))))

Function: vl-emodwire-encoded$inline

(defun vl-emodwire-encoded$inline (basename index)
 (declare
      (type string basename)
      (xargs :guard (and (maybe-natp index)
                         (or index (not (equal basename "NIL"))))))
 (mbe
     :logic
     (if (not index)
         (intern basename "ACL2")
       (intern (cat basename "[" (natstr index) "]")
               "ACL2"))
     :exec
     (cond ((not index) (intern basename "ACL2"))
           ((< index 256)
            (intern (cat basename
                         (aref1 '*vl-indexed-wire-name-array*
                                *vl-indexed-wire-name-array* index))
                    "ACL2"))
           (t (intern (cat basename "[" (natstr index) "]")
                      "ACL2")))))

Theorem: vl-emodwire-p-of-vl-emodwire-encoded

(defthm vl-emodwire-p-of-vl-emodwire-encoded
  (implies
       (and (force (stringp name))
            (force (maybe-natp index))
            (force (or index (not (equal name "NIL")))))
       (vl-emodwire-p (vl-emodwire-encoded (vl-emodwire-encode name)
                                           index))))

Function: vl-emodwire-exec$inline

(defun vl-emodwire-exec$inline (basename index)
  (declare
       (type string basename)
       (xargs :guard (and (maybe-natp index)
                          (or index (not (equal basename "NIL"))))))
  (vl-emodwire-encoded (vl-emodwire-encode basename)
                       index))

Theorem: vl-emodwire-p-of-vl-emodwire-exec

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

Function: vl-emodwire

(defun vl-emodwire (basename index)
  (declare
       (type string basename)
       (xargs :guard (and (maybe-natp index)
                          (or index (not (equal basename "NIL"))))))
  (mbe :logic
       (let ((basename (vl-emodwire-encode basename)))
         (if (not index)
             (intern basename "ACL2")
           (intern (cat basename "[" (natstr index) "]")
                   "ACL2")))
       :exec (vl-emodwire-exec basename index)))

Theorem: vl-emodwire-is-vl-emodwire-exec

(defthm vl-emodwire-is-vl-emodwire-exec
  (equal (vl-emodwire basename index)
         (vl-emodwire-exec basename index)))

Theorem: symbolp-of-vl-emodwire

(defthm symbolp-of-vl-emodwire
  (symbolp (vl-emodwire basename index))
  :rule-classes :type-prescription)

Theorem: vl-emodwire-p-of-vl-emodwire

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