		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl::vl-design-sv-use-set

Analyze used/set variables using SV's semantics.

Signature
(vl::vl-design-sv-use-set vl::x vl::modalist) → vl::new-x
Arguments: vl::x — Guard (vl::vl-design-p vl::x).; vl::modalist — Guard (modalist-p vl::modalist).
Returns: vl::new-x — Type (vl::vl-design-p vl::new-x).

This check issues warnings about variables that are unused, unset, or spurious (neither used nor set). It has some overlap with vl::lucid, but each check does some things that the other doesn't:

Lucid checks whether parameters, functions, types, etc. are used, whereas sv-use-set only deals with variables (a category which includes wires and regs, etc).
Lucid checks variables that are local to procedural code, which sv-use-set currently does not.
Sv-use-set understands complex datatypes and is exact in its analysis of which array/struct/etc. fields are used/set, which lucid does not.
Sv-use-set understands procedural constructs such as bounded loops and in many cases can statically determine which indices of an array are accessed even when the index is a local procedural variable.

Definitions and Theorems

Function: vl-design-sv-use-set

(defun vl::vl-design-sv-use-set (vl::x vl::modalist)
 (declare (xargs :guard (and (vl::vl-design-p vl::x)
                             (modalist-p vl::modalist))))
 (declare
      (xargs :guard (svarlist-addr-p (modalist-vars vl::modalist))))
 (let ((__function__ 'vl::vl-design-sv-use-set))
   (declare (ignorable __function__))
   (b*
     ((vl::modalist (modalist-fix vl::modalist))
      ((unless (modhier-loopfreelist-p (alist-keys vl::modalist)
                                       vl::modalist))
       (cw "Error: loop in instantiation hierarchy??~%")
       (vl::vl-design-fix vl::x))
      ((mv vl::stubbed-modalist
           vl::use-set-acc vl::reportcard)
       (sv-use-set-analyze-all vl::modalist vl::modalist nil nil
                               nil (vl::vl-scopestack-init vl::x))))
     (fast-alist-free vl::stubbed-modalist)
     (fast-alist-free vl::use-set-acc)
     (vl::vl-apply-reportcard vl::x vl::reportcard))))

Theorem: vl-design-p-of-vl-design-sv-use-set

(defthm vl::vl-design-p-of-vl-design-sv-use-set
  (b* ((vl::new-x (vl::vl-design-sv-use-set vl::x vl::modalist)))
    (vl::vl-design-p vl::new-x))
  :rule-classes :rewrite)

Theorem: vl-design-sv-use-set-of-vl-design-fix-x

(defthm vl::vl-design-sv-use-set-of-vl-design-fix-x
  (equal (vl::vl-design-sv-use-set (vl::vl-design-fix vl::x)
                                   vl::modalist)
         (vl::vl-design-sv-use-set vl::x vl::modalist)))

Theorem: vl-design-sv-use-set-vl-design-equiv-congruence-on-x

(defthm vl::vl-design-sv-use-set-vl-design-equiv-congruence-on-x
  (implies
       (vl::vl-design-equiv vl::x vl::x-equiv)
       (equal (vl::vl-design-sv-use-set vl::x vl::modalist)
              (vl::vl-design-sv-use-set vl::x-equiv vl::modalist)))
  :rule-classes :congruence)

Theorem: vl-design-sv-use-set-of-modalist-fix-modalist

(defthm vl::vl-design-sv-use-set-of-modalist-fix-modalist
 (equal (vl::vl-design-sv-use-set vl::x (modalist-fix vl::modalist))
        (vl::vl-design-sv-use-set vl::x vl::modalist)))

Theorem: vl-design-sv-use-set-modalist-equiv-congruence-on-modalist

(defthm
     vl::vl-design-sv-use-set-modalist-equiv-congruence-on-modalist
  (implies
       (modalist-equiv vl::modalist vl::modalist-equiv)
       (equal (vl::vl-design-sv-use-set vl::x vl::modalist)
              (vl::vl-design-sv-use-set vl::x vl::modalist-equiv)))
  :rule-classes :congruence)