		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-custom-suppress-multidrive-p

Mechanism for custom suppression of multidrive warnings.

We use this at Centaur to suppress multidrive warnings within certain modules that we know are not RTL designs.

This is an attachable function that should return t when you want to suppress warnings. It can inspect:

ss - the scopestack for the declaration.
item - the variable or parameter declaration itself.
set - the list of places where the variable was set.

This suppression is done in addition to the default heuristics. That is, your function can focus just on the additional rules you want to add, and doesn't have to recreate the default heuristics.

Definitions and Theorems

Theorem: booleanp-of-vl-custom-suppress-multidrive-p

(defthm booleanp-of-vl-custom-suppress-multidrive-p
  (booleanp (vl-custom-suppress-multidrive-p ss item set))
  :rule-classes :type-prescription)

Function: vl-custom-suppress-multidrive-p-default

(defun vl-custom-suppress-multidrive-p-default (ss item set)
  (declare (xargs :guard (and (vl-scopestack-p ss)
                              (or (vl-paramdecl-p item)
                                  (vl-vardecl-p item))
                              (vl-lucidocclist-p set))))
  (declare (ignorable ss item set))
  (let ((__function__ 'vl-custom-suppress-multidrive-p-default))
    (declare (ignorable __function__))
    nil))

Theorem: vl-custom-suppress-multidrive-p-default-of-vl-scopestack-fix-ss

(defthm
    vl-custom-suppress-multidrive-p-default-of-vl-scopestack-fix-ss
 (equal
     (vl-custom-suppress-multidrive-p-default (vl-scopestack-fix ss)
                                              item set)
     (vl-custom-suppress-multidrive-p-default ss item set)))

Theorem: vl-custom-suppress-multidrive-p-default-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-custom-suppress-multidrive-p-default-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
       (vl-custom-suppress-multidrive-p-default ss item set)
       (vl-custom-suppress-multidrive-p-default ss-equiv item set)))
 :rule-classes :congruence)

Theorem: vl-custom-suppress-multidrive-p-default-of-vl-lucidocclist-fix-set

(defthm
 vl-custom-suppress-multidrive-p-default-of-vl-lucidocclist-fix-set
 (equal (vl-custom-suppress-multidrive-p-default
             ss item (vl-lucidocclist-fix set))
        (vl-custom-suppress-multidrive-p-default ss item set)))

Theorem: vl-custom-suppress-multidrive-p-default-vl-lucidocclist-equiv-congruence-on-set

(defthm
 vl-custom-suppress-multidrive-p-default-vl-lucidocclist-equiv-congruence-on-set
 (implies
  (vl-lucidocclist-equiv set set-equiv)
  (equal
       (vl-custom-suppress-multidrive-p-default ss item set)
       (vl-custom-suppress-multidrive-p-default ss item set-equiv)))
 :rule-classes :congruence)