		Search-engine friendly clone of the ACL2 documentation.

Vcd.lisp

Vcd-dump-first-snapshot

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

Definitions and Theorems

Function: vcd-dump-first-snapshot

(defun vcd-dump-first-snapshot (vcd-vals vcd-wiremap p)
  (declare (xargs :stobjs (vcd-vals vcd-wiremap)))
  (declare (xargs :guard (vl-printedlist-p p)))
  (declare (xargs :guard (<= (vcdwires-length vcd-wiremap)
                             (4vecs-length vcd-vals))))
  (let ((__function__ 'vcd-dump-first-snapshot))
    (declare (ignorable __function__))
    (b* ((p (rlist* p "$dumpvars" #\Newline))
         (p (vcd-dump-first-snapshot-aux 0 vcd-vals vcd-wiremap p)))
      (rlist* p "$end" #\Newline))))

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

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