• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
        • Defwellformed
        • Reasonable
          • Vl-modulelist-check-reasonable
          • Vl-vardecl-reasonable-p
          • Vl-portdecl-and-moduleitem-compatible-p
          • Vl-module-reasonable-p
          • Vl-overlap-compatible-p
          • Vl-module-check-reasonable
          • Vl-portlist-reasonable-p
          • Vl-vardecllist-reasonable-p
          • Vl-modulelist-reasonable-p
        • Lvaluecheck
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Reasonable

Vl-vardecl-reasonable-p

(vl-vardecl-reasonable-p x) determines if a vl-vardecl-p is reasonable.

We restrict wire declarations in the following ways:

• The only allowed types are supply0, supply1, and plain wires. Not permitted are types such as wor and tri0.
• Arrays of wires are not supported. (Note that we do support wires with ranges, e.g., wire [7:0] w. What we do not support are, e.g., wire w [7:0], or multi-dimensional arrays such as wire [7:0] w [3:0].

Definitions and Theorems

Function: vl-vardecl-reasonable-p

(defun vl-vardecl-reasonable-p (x)
  (declare (xargs :guard (vl-vardecl-p x)))
  (b* (((vl-vardecl x) x))
    (and (if (and (equal (vl-datatype-kind x.type)
                         :vl-coretype)
                  (member (vl-coretype->name x.type)
                          '(:vl-logic :vl-reg))
                  (member x.nettype
                          '(nil :vl-supply0 :vl-supply1 :vl-wire)))
             t
           nil)
         (if (let ((x.udims (vl-datatype->udims x.type))
                   (x.pdims (vl-datatype->pdims x.type)))
               (and (not x.udims)
                    (or (atom x.pdims)
                        (atom (cdr x.pdims)))))
             t
           nil)
         (if (vl-simplevar-p x) t nil))))

Function: vl-vardecl-reasonable-p-warn

(defun vl-vardecl-reasonable-p-warn (x warnings)
 (declare (xargs :guard (and (vl-vardecl-p x)
                             (vl-warninglist-p warnings)))
          (ignorable warnings))
 (b* (((vl-vardecl x) x))
  (b*
   (((mv __ok1__ warnings)
     (if (and (equal (vl-datatype-kind x.type)
                     :vl-coretype)
              (member (vl-coretype->name x.type)
                      '(:vl-logic :vl-reg))
              (member x.nettype
                      '(nil :vl-supply0 :vl-supply1 :vl-wire)))
         (mv t warnings)
      (mv
       nil
       (cons
         (make-vl-warning
              :type :vl-bad-variable
              :msg "~a0: wire has unsupported type ~a1/nettype ~a2."
              :args (list x x.type x.nettype))
         warnings))))
    ((mv __ok2__ warnings)
     (b*
      (((mv __ok1__ warnings)
        (if (let ((x.udims (vl-datatype->udims x.type))
                  (x.pdims (vl-datatype->pdims x.type)))
              (and (not x.udims)
                   (or (atom x.pdims)
                       (atom (cdr x.pdims)))))
            (mv t warnings)
          (mv nil
              (cons (make-vl-warning
                         :type :vl-bad-variable
                         :msg "~a0: arrays are not yet supported."
                         :args (list x))
                    warnings))))
       ((mv __ok2__ warnings)
        (b*
         (((mv __ok1__ warnings)
           (if (vl-simplevar-p x)
               (mv t warnings)
             (mv nil
                 (cons (make-vl-warning
                            :type :vl-bad-variable
                            :msg "~a0: variable is too complicated."
                            :args (list x))
                       warnings))))
          ((mv __ok2__ warnings) (mv t warnings)))
         (mv (and __ok1__ __ok2__) warnings))))
      (mv (and __ok1__ __ok2__) warnings))))
   (mv (and __ok1__ __ok2__) warnings))))

Theorem: eliminate-vl-vardecl-reasonable-p-warn

(defthm eliminate-vl-vardecl-reasonable-p-warn
  (equal (mv-nth 0
                 (vl-vardecl-reasonable-p-warn x warnings))
         (vl-vardecl-reasonable-p x)))

Theorem: vl-warninglist-p-of-vl-vardecl-reasonable-p-warn

(defthm vl-warninglist-p-of-vl-vardecl-reasonable-p-warn
 (implies (force (vl-warninglist-p warnings))
          (vl-warninglist-p
               (mv-nth 1
                       (vl-vardecl-reasonable-p-warn x warnings)))))