		Search-engine friendly clone of the ACL2 documentation.

Vl-reportcard

Vl-design-origname-reportcard

Constructs a vl-reportcard-p for a design in terms of original design element names.

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

This is like vl-design-reportcard but uses original, pre-unparameterized names where possible.

Unparameterization causes problems for printing warnings about each module, because, e.g., instead of having warnings about adder, we actually have warnings about adder$width=5 and adder$width=13, etc. Yet the end-user typically shouldn't be bothered with looking at the warnings for each specialized version of adder; he just wants to see all of the warnings.

This function gathers up all warnings associated with each module, and builds a vl-reportcard-p that maps orignames to warnings. We take care to ensure that all of the warnings associated with each name are properly cleaned up and merged.

Definitions and Theorems

Function: vl-design-origname-reportcard

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

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

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

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

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

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

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

Subtopics

Vl-design-origname-reportcard-aux: Extend a vl-reportcard-p with all of the warnings for a design, in terms of the original design element names.