• 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
            • Vl-msb-expr-bitlist
            • Vl-plain-wire-name
            • Vl-module-wirealist
            • Vl-emodwires-from-high-to-low
            • Vl-vardecl-msb-emodwires
            • Vl-vardecllist-to-wirealist
            • Vl-emodwires-from-msb-to-lsb
            • Vl-verilogify-emodwirelist
          • Emodwire-encoding
          • Vl-emodwire-p
          • 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-wirealist-p

Vl-vardecl-msb-emodwires

Compute the vl-emodwire-ps for a variable declaration, in MSB-first order.

Signature

(vl-vardecl-msb-emodwires x warnings) 
  → 
(mv successp warnings emodwires)

Arguments

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

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

Returns

successp — Type (booleanp successp).

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

emodwires — Type (vl-emodwirelist-p emodwires).

Definitions and Theorems

Function: vl-vardecl-msb-emodwires

(defun vl-vardecl-msb-emodwires (x warnings)
 (declare (xargs :guard (and (vl-vardecl-p x)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-vardecl-msb-emodwires))
  (declare (ignorable __function__))
  (b*
   (((vl-vardecl x) x)
    ((unless (vl-simplevar-p x))
     (mv
      nil
      (fatal
       :type :vl-bad-vardecl
       :msg
       "~a0 is not yet supported: we only handle simple ~
                         wires and reg/logic variables  with at most a single ~
                         range."
       :args (list x))
      nil))
    (range (vl-simplevar->range x))
    ((unless (vl-maybe-range-resolved-p range))
     (mv nil
         (fatal :type :vl-bad-vardecl
                :msg "~a0 has unresolved range ~a1."
                :args (list x range))
         nil))
    ((unless range)
     (mv t (ok)
         (list (vl-plain-wire-name x.name))))
    (msb (vl-resolved->val (vl-range->msb range)))
    (lsb (vl-resolved->val (vl-range->lsb range)))
    (|w[msb:lsb]| (vl-emodwires-from-msb-to-lsb x.name msb lsb)))
   (mv t (ok) |w[msb:lsb]|))))

Theorem: booleanp-of-vl-vardecl-msb-emodwires.successp

(defthm booleanp-of-vl-vardecl-msb-emodwires.successp
  (b* (((mv ?successp ?warnings ?emodwires)
        (vl-vardecl-msb-emodwires x warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-vardecl-msb-emodwires.warnings

(defthm vl-warninglist-p-of-vl-vardecl-msb-emodwires.warnings
  (b* (((mv ?successp ?warnings ?emodwires)
        (vl-vardecl-msb-emodwires x warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-emodwirelist-p-of-vl-vardecl-msb-emodwires.emodwires

(defthm vl-emodwirelist-p-of-vl-vardecl-msb-emodwires.emodwires
  (b* (((mv ?successp ?warnings ?emodwires)
        (vl-vardecl-msb-emodwires x warnings)))
    (vl-emodwirelist-p emodwires))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-vardecl-msb-emodwires

(defthm true-listp-of-vl-vardecl-msb-emodwires
  (true-listp (mv-nth 2
                      (vl-vardecl-msb-emodwires x warnings)))
  :rule-classes :type-prescription)

Theorem: basenames-of-vl-vardecl-msb-emodwires

(defthm basenames-of-vl-vardecl-msb-emodwires
  (implies
       (vl-vardecl-p x)
       (let ((wires (mv-nth 2
                            (vl-vardecl-msb-emodwires x warnings))))
         (equal (vl-emodwirelist->basenames wires)
                (replicate (len wires)
                           (vl-vardecl->name x))))))

Theorem: unique-indicies-of-vl-vardecl-msb-emodwires

(defthm unique-indicies-of-vl-vardecl-msb-emodwires
  (no-duplicatesp-equal
       (vl-emodwirelist->indices
            (mv-nth 2
                    (vl-vardecl-msb-emodwires x warnings)))))