		Search-engine friendly clone of the ACL2 documentation.

Vcd.lisp

Vcd-dump-delta-aux

Signature
(vcd-dump-delta-aux changes vcd-vals vcd-wiremap p) → p1
Arguments: changes — Guard (nat-listp changes).; p — Guard (vl-printedlist-p p).
Returns: p1 — Type (vl-printedlist-p p1).

Definitions and Theorems

Function: vcd-dump-delta-aux

(defun vcd-dump-delta-aux (changes vcd-vals vcd-wiremap p)
  (declare (xargs :stobjs (vcd-vals vcd-wiremap)))
  (declare (xargs :guard (and (nat-listp changes)
                              (vl-printedlist-p p))))
  (declare
       (xargs :guard (and (<= (vcdwires-length vcd-wiremap)
                              (4vecs-length vcd-vals))
                          (or (atom changes)
                              (< (nat-list-max changes)
                                 (vcdwires-length vcd-wiremap))))))
  (let ((__function__ 'vcd-dump-delta-aux))
    (declare (ignorable __function__))
    (b* (((when (atom changes))
          (vl::vl-printedlist-fix p))
         (n (car changes))
         (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-delta-aux (cdr changes)
                              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-delta-aux (cdr changes)
                          vcd-vals vcd-wiremap p))))

Theorem: vl-printedlist-p-of-vcd-dump-delta-aux

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

Theorem: vcd-dump-delta-aux-of-nat-list-fix-changes

(defthm vcd-dump-delta-aux-of-nat-list-fix-changes
  (equal (vcd-dump-delta-aux (acl2::nat-list-fix changes)
                             vcd-vals vcd-wiremap p)
         (vcd-dump-delta-aux changes vcd-vals vcd-wiremap p)))

Theorem: vcd-dump-delta-aux-nat-list-equiv-congruence-on-changes

(defthm vcd-dump-delta-aux-nat-list-equiv-congruence-on-changes
 (implies
  (acl2::nat-list-equiv changes changes-equiv)
  (equal (vcd-dump-delta-aux changes vcd-vals vcd-wiremap p)
         (vcd-dump-delta-aux changes-equiv vcd-vals vcd-wiremap p)))
 :rule-classes :congruence)