		Search-engine friendly clone of the ACL2 documentation.

Designwires

Vl-vardecl-designwires

Add a VL_DESIGN_WIRE attribute to a vl-vardecl-p.

Signature
(vl-vardecl-designwires x) → new-x
Arguments: x — Guard (vl-vardecl-p x).
Returns: new-x — Type (vl-vardecl-p new-x).

Definitions and Theorems

Function: vl-vardecl-designwires

(defun vl-vardecl-designwires (x)
  (declare (xargs :guard (vl-vardecl-p x)))
  (let ((__function__ 'vl-vardecl-designwires))
    (declare (ignorable __function__))
    (b* (((vl-vardecl x) (vl-vardecl-fix x))
         ((when (assoc-equal "VL_DESIGN_WIRE" x.atts))
          x)
         (atts (acons "VL_DESIGN_WIRE" nil x.atts)))
      (change-vl-vardecl x :atts atts))))

Theorem: vl-vardecl-p-of-vl-vardecl-designwires

(defthm vl-vardecl-p-of-vl-vardecl-designwires
  (b* ((new-x (vl-vardecl-designwires x)))
    (vl-vardecl-p new-x))
  :rule-classes :rewrite)

Theorem: vl-vardecl-designwires-of-vl-vardecl-fix-x

(defthm vl-vardecl-designwires-of-vl-vardecl-fix-x
  (equal (vl-vardecl-designwires (vl-vardecl-fix x))
         (vl-vardecl-designwires x)))

Theorem: vl-vardecl-designwires-vl-vardecl-equiv-congruence-on-x

(defthm vl-vardecl-designwires-vl-vardecl-equiv-congruence-on-x
  (implies (vl-vardecl-equiv x x-equiv)
           (equal (vl-vardecl-designwires x)
                  (vl-vardecl-designwires x-equiv)))
  :rule-classes :congruence)