		Search-engine friendly clone of the ACL2 documentation.

Vl-module-p

Vl-module->hands-offp

Attribute that says a module should not be transformed.

Signature
(vl-module->hands-offp x) → hands-offp
Arguments: x — Guard (vl-module-p x).

We use the ordinary attribute VL_HANDS_OFF to say that a module should not be changed by transforms.

This is generally meant for use in VL primitives. The Verilog definitions of these modules sometimes make use of fancy Verilog constructs. Normally our transforms would try to remove these constructs, replacing them with instances of primitives. This can lead to funny sorts of problems if we try to transform the primitives themselves.

For instance, consider the *vl-1-bit-delay-1* module. This module has a delayed assignment, assign #1 out = in. If we hit this module with the delayredux transform, we'll try to replace the delay with an explicit instance of VL_1_BIT_DELAY_1. But that's crazy: now the module is trying to instantiate itself!

Similar issues can arise from trying to replace the always statements in a primitive flop/latch with instances of flop/latch primitives, etc. So as a general rule, we mark the primitives with VL_HANDS_OFF and code our transforms to not modules with this attribute.

Definitions and Theorems

Function: vl-module->hands-offp$inline

(defun vl-module->hands-offp$inline (x)
  (declare (xargs :guard (vl-module-p x)))
  (let ((__function__ 'vl-module->hands-offp))
    (declare (ignorable __function__))
    (consp (assoc-equal "VL_HANDS_OFF" (vl-module->atts x)))))

Theorem: vl-module->hands-offp$inline-of-vl-module-fix-x

(defthm vl-module->hands-offp$inline-of-vl-module-fix-x
  (equal (vl-module->hands-offp$inline (vl-module-fix x))
         (vl-module->hands-offp$inline x)))

Theorem: vl-module->hands-offp$inline-vl-module-equiv-congruence-on-x

(defthm vl-module->hands-offp$inline-vl-module-equiv-congruence-on-x
  (implies (vl-module-equiv x x-equiv)
           (equal (vl-module->hands-offp$inline x)
                  (vl-module->hands-offp$inline x-equiv)))
  :rule-classes :congruence)