		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.