		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-atts-find-paramname

Signature
(vl-atts-find-paramname atts) → paramname
Arguments: atts — Guard (vl-atts-p atts).
Returns: paramname — Type (maybe-stringp paramname).

Definitions and Theorems

Function: vl-atts-find-paramname

(defun vl-atts-find-paramname (atts)
 (declare (xargs :guard (vl-atts-p atts)))
 (let ((__function__ 'vl-atts-find-paramname))
  (declare (ignorable __function__))
  (b* ((look (hons-assoc-equal "VL_PARAMNAME" (vl-atts-fix atts)))
       ((unless look) nil)
       (val (cdr look))
       ((unless val) nil))
   (vl-expr-case val
                 :vl-literal (vl-value-case val.val
                                            :vl-string val.val.value
                                            :otherwise nil)
                 :otherwise nil))))

Theorem: maybe-stringp-of-vl-atts-find-paramname

(defthm maybe-stringp-of-vl-atts-find-paramname
  (b* ((paramname (vl-atts-find-paramname atts)))
    (maybe-stringp paramname))
  :rule-classes :type-prescription)

Theorem: vl-atts-find-paramname-of-vl-atts-fix-atts

(defthm vl-atts-find-paramname-of-vl-atts-fix-atts
  (equal (vl-atts-find-paramname (vl-atts-fix atts))
         (vl-atts-find-paramname atts)))

Theorem: vl-atts-find-paramname-vl-atts-equiv-congruence-on-atts

(defthm vl-atts-find-paramname-vl-atts-equiv-congruence-on-atts
  (implies (vl-atts-equiv atts atts-equiv)
           (equal (vl-atts-find-paramname atts)
                  (vl-atts-find-paramname atts-equiv)))
  :rule-classes :congruence)