		Search-engine friendly clone of the ACL2 documentation.

Vcd.lisp

Vcd-print-wiredecls

Signature
(vcd-print-wiredecls x p) → p1
Arguments: x — Guard (vcd-wirelist-p x).; p — Guard (vl-printedlist-p p).
Returns: p1 — Type (vl-printedlist-p p1).

Definitions and Theorems

Function: vcd-print-wiredecls

(defun vcd-print-wiredecls (x p)
  (declare (xargs :guard (and (vcd-wirelist-p x)
                              (vl-printedlist-p p))))
  (let ((__function__ 'vcd-print-wiredecls))
    (declare (ignorable __function__))
    (b* (((when (atom x))
          (vl::vl-printedlist-fix p))
         ((vcd-wire xf) (car x))
         (p (rlist* p "$var wire "
                    (natstr (vcd-wire->width (car x)))
                    " " xf.code " " xf.name))
         (p (cond ((and (eql xf.msb 0) (eql xf.lsb 0)) p)
                  ((eql xf.msb xf.lsb)
                   (rlist* p "[" (if (< xf.msb 0) "-" "")
                           (natstr (abs xf.msb))
                           "]"))
                  (t (rlist* p "[" (if (< xf.msb 0) "-" "")
                             (natstr (abs xf.msb))
                             ":" (if (< xf.lsb 0) "-" "")
                             (natstr (abs xf.lsb))
                             "]"))))
         (p (rlist* p " $end" #\Newline)))
      (vcd-print-wiredecls (cdr x) p))))

Theorem: vl-printedlist-p-of-vcd-print-wiredecls

(defthm vl-printedlist-p-of-vcd-print-wiredecls
  (b* ((p1 (vcd-print-wiredecls x p)))
    (vl-printedlist-p p1))
  :rule-classes :rewrite)

Theorem: vcd-print-wiredecls-of-vcd-wirelist-fix-x

(defthm vcd-print-wiredecls-of-vcd-wirelist-fix-x
  (equal (vcd-print-wiredecls (vcd-wirelist-fix x)
                              p)
         (vcd-print-wiredecls x p)))

Theorem: vcd-print-wiredecls-vcd-wirelist-equiv-congruence-on-x

(defthm vcd-print-wiredecls-vcd-wirelist-equiv-congruence-on-x
  (implies (vcd-wirelist-equiv x x-equiv)
           (equal (vcd-print-wiredecls x p)
                  (vcd-print-wiredecls x-equiv p)))
  :rule-classes :congruence)