Cross-check ports against port declarations for traditional UDPs.
(vl-make-traditional-udp-head name portids decls) → (mv warning head)
Function:
(defun vl-make-traditional-udp-head (name portids decls) (declare (xargs :guard (and (vl-idtoken-p name) (vl-idtoken-list-p portids) (vl-port/vardecllist-p decls)))) (let ((__function__ 'vl-make-traditional-udp-head)) (declare (ignorable __function__)) (b* ((loc (vl-token->loc name)) (udpname (vl-idtoken->name name)) (portdecls (vl-port/vardecllist->portdecls decls)) (vardecls (vl-port/vardecllist->vardecls decls)) (idnames (vl-idtokenlist->names portids)) (pdnames (vl-portdecllist->names portdecls)) ((unless (<= 2 (len idnames))) (mv (make-vl-warning :type :vl-bad-udp :msg "~a0: primitive ~m1 must have at least one ~ output and one input port." :args (list loc udpname) :fatalp t :fn __function__) nil)) ((unless (uniquep idnames)) (mv (make-vl-warning :type :vl-bad-udp :msg "~a0: primitive ~m1 has duplicate ports: ~&2." :args (list loc udpname (duplicated-members idnames)) :fatalp t :fn __function__) nil)) ((unless (uniquep pdnames)) (mv (make-vl-warning :type :vl-bad-udp :msg "~a0: primitive ~m1 multiply declares ports: ~&2." :args (list loc udpname (duplicated-members pdnames)) :fatalp t :fn __function__) nil)) ((unless (or (atom vardecls) (atom (cdr vardecls)))) (mv (make-vl-warning :type :vl-bad-udp :msg "~a0: primitive ~m1 has ~x2 reg declareations, but ~ only one is allowed." :args (list loc udpname (len vardecls)) :fatalp t :fn __function__) nil)) ((unless (equal (mergesort idnames) (mergesort pdnames))) (mv (make-vl-warning :type :vl-bad-udp :msg "~a0: ports for primitive ~m1 don't line up with ~ its port declarations.~% ~ - Ports without declarations: ~&2~% ~ - Declarations without ports: ~&3~%" :args (list loc udpname (difference (mergesort idnames) (mergesort pdnames)) (difference (mergesort pdnames) (mergesort idnames))) :fatalp t :fn __function__) nil)) (outname (car idnames)) (outdecl (vl-find-portdecl outname portdecls)) (indecls (vl-portdecls-with-dir :vl-input portdecls)) ((unless (equal (vl-portdecl->dir outdecl) :vl-output)) (mv (make-vl-warning :type :vl-bad-udp :msg "~a0: first port of primitive ~m1, ~w2, must be an output." :args (list loc udpname outname) :fatalp t :fn __function__) nil)) (expected-innames (mergesort (cdr idnames))) (declared-innames (mergesort (vl-portdecllist->names indecls))) ((unless (equal expected-innames declared-innames)) (mv (make-vl-warning :type :vl-bad-udp :msg "~a0: ports of primitive ~m1 after the first (~w2) are not declared as inputs: ~&3." :args (list loc udpname outname (difference expected-innames declared-innames)) :fatalp t :fn __function__) nil)) ((unless (or (atom vardecls) (equal (vl-vardecl->name (car vardecls)) outname))) (mv (make-vl-warning :type :vl-bad-udp :msg "~a0: primitive ~m1 has a reg declaration for ~w2 ~ which is not its output ~w3." :args (list loc udpname (vl-vardecl->name (car vardecls)) outname) :fatalp t :fn __function__) nil)) (outdecl-regp (equal (vl-portdecl->type outdecl) *vl-plain-old-reg-type*)) (vardecl-p (consp vardecls)) ((when (and outdecl-regp vardecl-p)) (mv (make-vl-warning :type :vl-bad-udp :msg "~a0: primitive ~m1 explicitly declares ~w2 as ~ an output reg, so it must not also have a ~ separate reg declaration." :args (list loc udpname outname) :fatalp t :fn __function__) nil)) (outdecl (if vardecl-p (change-vl-portdecl outdecl :type *vl-plain-old-reg-type*) outdecl)) (sequentialp (equal (vl-portdecl->type outdecl) *vl-plain-old-reg-type*)) (indecls (vl-reorder-portdecls (cdr idnames) indecls))) (mv nil (make-vl-udp-head :output outdecl :inputs indecls :sequentialp sequentialp)))))
Theorem:
(defthm return-type-of-vl-make-traditional-udp-head.warning (b* (((mv common-lisp::?warning set::?head) (vl-make-traditional-udp-head name portids decls))) (and (implies warning (not head)) (iff (vl-warning-p warning) warning))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-make-traditional-udp-head.head (implies (and (force (vl-idtoken-p name)) (force (vl-idtoken-list-p portids)) (force (vl-port/vardecllist-p decls))) (b* (((mv common-lisp::?warning set::?head) (vl-make-traditional-udp-head name portids decls))) (implies (not warning) (vl-udp-head-p head)))) :rule-classes :rewrite)