Human-readable description of what kind of module element this is.
(vl-modelement->short-kind-string x) → str
Function:
(defun vl-modelement->short-kind-string (x) (declare (xargs :guard (vl-modelement-p x))) (let ((__function__ 'vl-modelement->short-kind-string)) (declare (ignorable __function__)) (case (tag x) (:vl-portdecl "port declaration") (:vl-assign "continuous assignment") (:vl-alias "alias declaration") (:vl-vardecl "variable declaration") (:vl-paramdecl "parameter declaration") (:vl-fundecl "function declaration") (:vl-taskdecl "task declaration") (:vl-modinst "module instance") (:vl-gateinst "gate instance") (:vl-always "always statement") (:vl-initial "initial statement") (:vl-final "final statement") (:vl-typedef "typedef") (:vl-fwdtypedef "forward typedef") (:vl-import "package import") (:vl-modport "modport declaration") (:vl-genvar "genvar declaration") (:vl-assertion "immediate assertion") (:vl-cassertion "concurrent assertion") (:vl-property "property declaration") (:vl-sequence "sequence declaration") (:vl-clkdecl "clocking declaration") (:vl-gclkdecl "global clocking declaration") (:vl-defaultdisable "default disable") (:vl-dpiimport "DPI import") (:vl-dpiexport "DPI export") (:vl-bind "bind declaration") (:vl-class "class declaration") (:vl-covergroup "covergroup") (:vl-elabtask "elaborate (e.g., $fatal, ...) system task") (:vl-letdecl "let declaration") (otherwise (progn$ (impossible) "invalid")))))
Theorem:
(defthm stringp-of-vl-modelement->short-kind-string (b* ((str (vl-modelement->short-kind-string x))) (stringp str)) :rule-classes :type-prescription)