		Search-engine friendly clone of the ACL2 documentation.

Sv-ansi-port-interpretation

Vl-process-first-ansi-port

Signature
(vl-process-first-ansi-port x) → (mv ifacep ports-acc portdecls-acc vardecls-acc)
Arguments: x — Guard (vl-parsed-ansi-port-p x).
Returns: ifacep — Was this port an interface port?.
Type (booleanp ifacep).; ports-acc — Type (and (vl-portlist-p ports-acc) (consp ports-acc) (equal (vl-interfaceport-p (car ports-acc)) ifacep) (equal (vl-regularport-p (car ports-acc)) (not ifacep))) .; portdecls-acc — Type (and (vl-portdecllist-p portdecls-acc) (implies (not ifacep) (consp portdecls-acc))) .; vardecls-acc — Type (and (vl-vardecllist-p vardecls-acc) (implies (not ifacep) (consp vardecls-acc))) .

Note: we assume that the first port in the list has at least a direction, port kind, or data type. Otherwise, per Section 23.2.2.3, the ports are supposed to be assumed to be a non-ANSI style list of ports, so we shouldn't be trying to parse the ports as a list of ansi ports at all!

Definitions and Theorems

Function: vl-process-first-ansi-port

(defun vl-process-first-ansi-port (x)
 (declare (xargs :guard (vl-parsed-ansi-port-p x)))
 (let ((__function__ 'vl-process-first-ansi-port))
  (declare (ignorable __function__))
  (b* (((vl-parsed-ansi-port x))
       ((vl-parsed-port-identifier x.id))
       (name (vl-idtoken->name x.id.name))
       (loc (vl-token->loc x.id.name)))
   (case
    (tag x.head)
    (:vl-parsed-interface-head
     (b*
      ((new-port
            (make-vl-interfaceport
                 :name name
                 :ifname (vl-parsed-interface-head->ifname x.head)
                 :modport (vl-parsed-interface-head->modport x.head)
                 :udims x.id.udims
                 :loc loc)))
      (mv t (list new-port) nil nil)))
    (:vl-parsed-portdecl-head
     (b*
      (((vl-parsed-portdecl-head x.head))
       (ports
           (list (make-vl-regularport :name name
                                      :expr (vl-idexpr name nil nil)
                                      :loc loc)))
       (complete-p t)
       (dir (or x.dir :vl-inout))
       (nettype (vl-nettype-for-parsed-ansi-port dir x.head))
       (type x.head.type)
       ((cons portdecls vardecls)
        (vl-make-ports-and-maybe-nets (list x.id)
                                      :dir dir
                                      :nettype nettype
                                      :type type
                                      :complete-p complete-p
                                      :atts x.atts)))
      (mv nil ports portdecls vardecls)))
    (otherwise
         (progn$ (impossible)
                 (mv t
                     (list (make-vl-interfaceport :name "bogus"
                                                  :ifname "bogus"))
                     nil nil)))))))

Theorem: booleanp-of-vl-process-first-ansi-port.ifacep

(defthm booleanp-of-vl-process-first-ansi-port.ifacep
  (b* (((mv ?ifacep
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-first-ansi-port x)))
    (booleanp ifacep))
  :rule-classes :type-prescription)

Theorem: return-type-of-vl-process-first-ansi-port.ports-acc

(defthm return-type-of-vl-process-first-ansi-port.ports-acc
  (b* (((mv ?ifacep
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-first-ansi-port x)))
    (and (vl-portlist-p ports-acc)
         (consp ports-acc)
         (equal (vl-interfaceport-p (car ports-acc))
                ifacep)
         (equal (vl-regularport-p (car ports-acc))
                (not ifacep))))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-process-first-ansi-port.portdecls-acc

(defthm return-type-of-vl-process-first-ansi-port.portdecls-acc
  (b* (((mv ?ifacep
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-first-ansi-port x)))
    (and (vl-portdecllist-p portdecls-acc)
         (implies (not ifacep)
                  (consp portdecls-acc))))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-process-first-ansi-port.vardecls-acc

(defthm return-type-of-vl-process-first-ansi-port.vardecls-acc
  (b* (((mv ?ifacep
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-first-ansi-port x)))
    (and (vl-vardecllist-p vardecls-acc)
         (implies (not ifacep)
                  (consp vardecls-acc))))
  :rule-classes :rewrite)