		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-occform-mkport

Helper for creating ports in generated modules.

Signature
(vl-occform-mkport name dir width) → (mv expr port portdecl vardecl)
Arguments: name — Guard (stringp name).; dir — Guard (vl-direction-p dir).; width — Guard (posp width).
Returns: expr — Type (vl-expr-p expr).; port — Type (vl-port-p port).; portdecl — Type (vl-portdecl-p portdecl).; vardecl — Type (vl-vardecl-p vardecl).

Imagine that we are trying to programmatically generate a module, and we want to add a port with the given name, direction, and width. This function just generates the corresponding expression, port, port declaration, and net declaration.

Definitions and Theorems

Function: vl-occform-mkport

(defun vl-occform-mkport (name dir width)
  (declare (xargs :guard (and (stringp name)
                              (vl-direction-p dir)
                              (posp width))))
  (let ((__function__ 'vl-occform-mkport))
    (declare (ignorable __function__))
    (b* ((name (hons-copy (string-fix name)))
         (width (lposfix width))
         (expr (vl-idexpr name width :vl-unsigned))
         (range (vl-make-n-bit-range width))
         (type (hons-copy (make-vl-coretype :name :vl-logic
                                            :signedp nil
                                            :pdims (list range))))
         (port (make-vl-regularport :name name
                                    :expr expr
                                    :loc *vl-fakeloc*))
         (portdecl (make-vl-portdecl :name name
                                     :type type
                                     :dir dir
                                     :loc *vl-fakeloc*))
         (vardecl (make-vl-vardecl :name name
                                   :type type
                                   :nettype :vl-wire
                                   :loc *vl-fakeloc*
                                   :atts '(("VL_PORT_IMPLICIT")))))
      (mv expr port portdecl vardecl))))

Theorem: vl-expr-p-of-vl-occform-mkport.expr

(defthm vl-expr-p-of-vl-occform-mkport.expr
  (b* (((mv ?expr ?port ?portdecl ?vardecl)
        (vl-occform-mkport name dir width)))
    (vl-expr-p expr))
  :rule-classes :rewrite)

Theorem: vl-port-p-of-vl-occform-mkport.port

(defthm vl-port-p-of-vl-occform-mkport.port
  (b* (((mv ?expr ?port ?portdecl ?vardecl)
        (vl-occform-mkport name dir width)))
    (vl-port-p port))
  :rule-classes :rewrite)

Theorem: vl-portdecl-p-of-vl-occform-mkport.portdecl

(defthm vl-portdecl-p-of-vl-occform-mkport.portdecl
  (b* (((mv ?expr ?port ?portdecl ?vardecl)
        (vl-occform-mkport name dir width)))
    (vl-portdecl-p portdecl))
  :rule-classes :rewrite)

Theorem: vl-vardecl-p-of-vl-occform-mkport.vardecl

(defthm vl-vardecl-p-of-vl-occform-mkport.vardecl
  (b* (((mv ?expr ?port ?portdecl ?vardecl)
        (vl-occform-mkport name dir width)))
    (vl-vardecl-p vardecl))
  :rule-classes :rewrite)

Theorem: vl-occform-mkport-of-str-fix-name

(defthm vl-occform-mkport-of-str-fix-name
  (equal (vl-occform-mkport (str-fix name)
                            dir width)
         (vl-occform-mkport name dir width)))

Theorem: vl-occform-mkport-streqv-congruence-on-name

(defthm vl-occform-mkport-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-occform-mkport name dir width)
                  (vl-occform-mkport name-equiv dir width)))
  :rule-classes :congruence)

Theorem: vl-occform-mkport-of-vl-direction-fix-dir

(defthm vl-occform-mkport-of-vl-direction-fix-dir
  (equal (vl-occform-mkport name (vl-direction-fix dir)
                            width)
         (vl-occform-mkport name dir width)))

Theorem: vl-occform-mkport-vl-direction-equiv-congruence-on-dir

(defthm vl-occform-mkport-vl-direction-equiv-congruence-on-dir
  (implies (vl-direction-equiv dir dir-equiv)
           (equal (vl-occform-mkport name dir width)
                  (vl-occform-mkport name dir-equiv width)))
  :rule-classes :congruence)

Theorem: vl-occform-mkport-of-pos-fix-width

(defthm vl-occform-mkport-of-pos-fix-width
  (equal (vl-occform-mkport name dir (pos-fix width))
         (vl-occform-mkport name dir width)))

Theorem: vl-occform-mkport-pos-equiv-congruence-on-width

(defthm vl-occform-mkport-pos-equiv-congruence-on-width
  (implies (acl2::pos-equiv width width-equiv)
           (equal (vl-occform-mkport name dir width)
                  (vl-occform-mkport name dir width-equiv)))
  :rule-classes :congruence)