Attribute that says a module should not be transformed.
(vl-module->hands-offp x) → hands-offp
We use the ordinary
This is probably mostly outdated. It was originally intended for use in vl2014::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 vl2014::*vl-1-bit-delay-1* module. This
module has a delayed assignment,
Similar issues can arise from trying to replace the
(defun vl-module->hands-offp$inline (x) (declare (xargs :guard (vl-module-p x))) (let ((__function__ 'vl-module->hands-offp)) (declare (ignorable __function__)) (consp (hons-assoc-equal "VL_HANDS_OFF" (vl-module->atts 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)))
(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)