		Search-engine friendly clone of the ACL2 documentation.

Vl-reportcard

Vl-design-reportcard

Constructs a vl-reportcard-p for a design.

Signature
(vl-design-reportcard x) → reportcard
Arguments: x — Guard (vl-design-p x).
Returns: reportcard — Already cleaned.
Type (vl-reportcard-p reportcard).

This reportcard is in terms of elaborated (unparameterized) names; see also vl-design-origname-reportcard for an alternative that uses original names.

Definitions and Theorems

Function: vl-design-reportcard

(defun vl-design-reportcard (x)
  (declare (xargs :guard (vl-design-p x)))
  (let ((__function__ 'vl-design-reportcard))
    (declare (ignorable __function__))
    (b* ((acc nil)
         (acc (vl-design-reportcard-aux x acc))
         (ret (vl-clean-reportcard acc)))
      (fast-alist-free acc)
      ret)))

Theorem: vl-reportcard-p-of-vl-design-reportcard

(defthm vl-reportcard-p-of-vl-design-reportcard
  (b* ((reportcard (vl-design-reportcard x)))
    (vl-reportcard-p reportcard))
  :rule-classes :rewrite)

Theorem: vl-design-reportcard-of-vl-design-fix-x

(defthm vl-design-reportcard-of-vl-design-fix-x
  (equal (vl-design-reportcard (vl-design-fix x))
         (vl-design-reportcard x)))

Theorem: vl-design-reportcard-vl-design-equiv-congruence-on-x

(defthm vl-design-reportcard-vl-design-equiv-congruence-on-x
  (implies (vl-design-equiv x x-equiv)
           (equal (vl-design-reportcard x)
                  (vl-design-reportcard x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-design-reportcard-aux: Extend a vl-reportcard-p with all of the warnings for a design.
Vl-modulelist-gather-origname-reportcard
Vl-typedeflist-gather-reportcard
Vl-programlist-gather-reportcard
Vl-packagelist-gather-reportcard
Vl-modulelist-gather-reportcard
Vl-interfacelist-gather-reportcard
Vl-configlist-gather-reportcard
Vl-udplist-gather-reportcard
Vl-classlist-gather-reportcard