		Search-engine friendly clone of the ACL2 documentation.

Vcd.lisp

Vcd-dump-first-snapshot-aux

Signature
(vcd-dump-first-snapshot-aux n vcd-vals vcd-wiremap p) → p1
Arguments: n — Guard (natp n).; p — Guard (vl-printedlist-p p).
Returns: p1 — Type (vl-printedlist-p p1).

Definitions and Theorems

Function: vcd-dump-first-snapshot-aux

(defun vcd-dump-first-snapshot-aux (n vcd-vals vcd-wiremap p)
 (declare (xargs :stobjs (vcd-vals vcd-wiremap)))
 (declare (xargs :guard (and (natp n) (vl-printedlist-p p))))
 (declare (xargs :guard (and (<= (vcdwires-length vcd-wiremap)
                                 (4vecs-length vcd-vals))
                             (<= n (vcdwires-length vcd-wiremap)))))
 (let ((__function__ 'vcd-dump-first-snapshot-aux))
   (declare (ignorable __function__))
   (b* (((when (mbe :logic (zp (- (vcdwires-length vcd-wiremap)
                                  (nfix n)))
                    :exec (eql (vcdwires-length vcd-wiremap) n)))
         (vl::vl-printedlist-fix p))
        (wire (get-vcdwire n vcd-wiremap))
        ((vcd-wire wire) wire)
        ((when (equal wire.code ""))
         (cw "~x0, ~s1: skipping wire with empty code~%"
             n wire.name)
         (vcd-dump-first-snapshot-aux (1+ (lnfix n))
                                      vcd-vals vcd-wiremap p))
        (wire.width (vcd-wire->width wire))
        (valstr (vcd-4vec-bitstr (get-4vec n vcd-vals)
                                 wire.width))
        (p (if (eql wire.width 1)
               (rlist* p valstr)
             (rlist* p #\b valstr #\Space)))
        (p (rlist* p wire.code #\Newline)))
     (vcd-dump-first-snapshot-aux (1+ (lnfix n))
                                  vcd-vals vcd-wiremap p))))

Theorem: vl-printedlist-p-of-vcd-dump-first-snapshot-aux

(defthm vl-printedlist-p-of-vcd-dump-first-snapshot-aux
  (b* ((p1 (vcd-dump-first-snapshot-aux n vcd-vals vcd-wiremap p)))
    (vl-printedlist-p p1))
  :rule-classes :rewrite)

Theorem: vcd-dump-first-snapshot-aux-of-nfix-n

(defthm vcd-dump-first-snapshot-aux-of-nfix-n
  (equal (vcd-dump-first-snapshot-aux (nfix n)
                                      vcd-vals vcd-wiremap p)
         (vcd-dump-first-snapshot-aux n vcd-vals vcd-wiremap p)))

Theorem: vcd-dump-first-snapshot-aux-nat-equiv-congruence-on-n

(defthm vcd-dump-first-snapshot-aux-nat-equiv-congruence-on-n
 (implies
  (nat-equiv n n-equiv)
  (equal
      (vcd-dump-first-snapshot-aux n vcd-vals vcd-wiremap p)
      (vcd-dump-first-snapshot-aux n-equiv vcd-vals vcd-wiremap p)))
 :rule-classes :congruence)