(vl-gatetype-names/dirs/assigns type nargs) → (mv err unimplemented assigns portnames portdirs)
Function:
(defun vl-gatetype-names/dirs/assigns (type nargs) (declare (xargs :guard (and (vl-gatetype-p type) (natp nargs)))) (let ((__function__ 'vl-gatetype-names/dirs/assigns)) (declare (ignorable __function__)) (b* ((nargs (lnfix nargs)) (type (vl-gatetype-fix type))) (case type ((:vl-cmos :vl-rcmos) (mv (if (eql nargs 4) nil (vmsg "Need 4 arguments for ~x0" type)) t nil '("out" "in" "ncontrol" "pcontrol") '(:vl-output :vl-input :vl-input :vl-input))) ((:vl-nmos :vl-rnmos :vl-pmos :vl-rpmos) (mv (if (eql nargs 3) nil (vmsg "Need 3 arguments for ~x0" type)) t nil '("out" "in" "control") '(:vl-output :vl-input :vl-input))) ((:vl-bufif0 :vl-bufif1 :vl-notif0 :vl-notif1) (b* (((unless (eql nargs 3)) (mv (vmsg "Need 3 arguments for ~x0" type) nil nil nil nil)) (ins '("data" "control")) (svex-ins (vl-fixup-wide-gate-inputs (svex-vars-from-names ins))) ((list data ctrl) svex-ins) (rhs (case type (:vl-bufif0 (sv::svcall sv::? ctrl (sv::svex-z) (sv::svcall sv::unfloat data))) (:vl-bufif1 (sv::svcall sv::? ctrl (sv::svcall sv::unfloat data) (sv::svex-z))) (:vl-notif0 (sv::svcall sv::? ctrl (sv::svex-z) (sv::svcall sv::bitnot data))) (:vl-notif1 (sv::svcall sv::? ctrl (sv::svcall sv::bitnot data) (sv::svex-z))))) (assigns (list (cons (svex-lhs-from-name "out") (sv::make-driver :value rhs)))) (portnames (cons "out" ins)) (portdirs (list :vl-output :vl-input :vl-input))) (mv nil nil assigns portnames portdirs))) ((:vl-and :vl-nand :vl-or :vl-nor :vl-xor :vl-xnor) (if (< nargs 2) (mv (vmsg "Need 2 or more arguments for ~x0" type) nil nil nil nil) (b* ((ins (vl-gatetypenames-count-up (1- nargs) 1 "in")) (svex-ins (vl-fixup-wide-gate-inputs (svex-vars-from-names ins))) (assigns (list (cons (svex-lhs-from-name "out") (if (eql (len svex-ins) 1) (sv::make-driver :value (case type ((:vl-and :vl-or :vl-xor) (sv::svcall sv::unfloat (car svex-ins))) ((:vl-nand :vl-nor :vl-xnor) (sv::svcall sv::bitnot (car svex-ins))))) (sv::make-driver :value (case type (:vl-and (svcall-join 'sv::bitand svex-ins)) (:vl-nand (sv::svcall sv::bitnot (svcall-join 'sv::bitand svex-ins))) (:vl-or (svcall-join 'sv::bitor svex-ins)) (:vl-nor (sv::svcall sv::bitnot (svcall-join 'sv::bitor svex-ins))) (:vl-xor (svcall-join 'sv::bitxor svex-ins)) (:vl-xnor (sv::svcall sv::bitnot (svcall-join 'sv::bitxor svex-ins))))))))) (portnames (cons "out" ins)) (portdirs (cons :vl-output (repeat (1- nargs) :vl-input)))) (mv nil nil assigns portnames portdirs)))) ((:vl-buf :vl-not) (if (< nargs 2) (mv (vmsg "Need 2 or more arguments for ~x0" type) nil nil nil nil) (b* ((outs (vl-gatetypenames-count-up (1- nargs) 1 "out")) (out-lhses (svex-lhses-from-names outs)) (in-var (svex-var-from-name "in")) (assigns (pairlis$ out-lhses (repeat (1- nargs) (sv::make-driver :value (case type (:vl-buf (sv::svcall sv::unfloat in-var)) (:vl-not (sv::svcall sv::bitnot in-var))))))) (portnames (append outs '("in"))) (portdirs (append (repeat (1- nargs) :vl-output) '(:vl-input)))) (mv nil nil assigns portnames portdirs)))) ((:vl-tranif0 :vl-tranif1 :vl-rtranif0 :vl-rtranif1) (mv (if (eql nargs 3) nil (vmsg "Need 3 arguments for ~x0" type)) t nil '("inout1" "inout2" "control") '(:vl-inout :vl-inout :vl-input))) ((:vl-tran :vl-rtran) (mv (if (eql nargs 2) nil (vmsg "Need 2 arguments for ~x0" type)) t nil '("inout1" "inout2") '(:vl-inout :vl-inout))) ((:vl-pullup :vl-pulldown) (mv (if (eql nargs 1) nil (vmsg "Need 1 argument for ~x0" type)) t nil '("net") '(:vl-inout))) (otherwise (prog2$ (impossible) (mv (vmsg "Impossible") nil nil nil nil)))))))
Theorem:
(defthm return-type-of-vl-gatetype-names/dirs/assigns.err (b* (((mv ?err ?unimplemented ?assigns ?portnames ?portdirs) (vl-gatetype-names/dirs/assigns type nargs))) (iff (vl-msg-p err) err)) :rule-classes :rewrite)
Theorem:
(defthm assigns-p-of-vl-gatetype-names/dirs/assigns.assigns (b* (((mv ?err ?unimplemented ?assigns ?portnames ?portdirs) (vl-gatetype-names/dirs/assigns type nargs))) (sv::assigns-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-gatetype-names/dirs/assigns.portnames (b* (((mv ?err ?unimplemented ?assigns ?portnames ?portdirs) (vl-gatetype-names/dirs/assigns type nargs))) (and (string-listp portnames) (implies (not err) (eql (len portnames) (nfix nargs))))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-gatetype-names/dirs/assigns.portdirs (b* (((mv ?err ?unimplemented ?assigns ?portnames ?portdirs) (vl-gatetype-names/dirs/assigns type nargs))) (and (vl-directionlist-p portdirs) (implies (not err) (eql (len portdirs) (nfix nargs))))) :rule-classes :rewrite)
Theorem:
(defthm svarlist-addr-p-of-vl-gatetype-names/dirs/assigns (b* (((mv ?err ?unimplemented ?assigns ?portnames ?portdirs) (vl-gatetype-names/dirs/assigns type nargs))) (sv::svarlist-addr-p (sv::assigns-vars assigns))))
Theorem:
(defthm vl-gatetype-names/dirs/assigns-of-vl-gatetype-fix-type (equal (vl-gatetype-names/dirs/assigns (vl-gatetype-fix type) nargs) (vl-gatetype-names/dirs/assigns type nargs)))
Theorem:
(defthm vl-gatetype-names/dirs/assigns-vl-gatetype-equiv-congruence-on-type (implies (vl-gatetype-equiv type type-equiv) (equal (vl-gatetype-names/dirs/assigns type nargs) (vl-gatetype-names/dirs/assigns type-equiv nargs))) :rule-classes :congruence)
Theorem:
(defthm vl-gatetype-names/dirs/assigns-of-nfix-nargs (equal (vl-gatetype-names/dirs/assigns type (nfix nargs)) (vl-gatetype-names/dirs/assigns type nargs)))
Theorem:
(defthm vl-gatetype-names/dirs/assigns-nat-equiv-congruence-on-nargs (implies (acl2::nat-equiv nargs nargs-equiv) (equal (vl-gatetype-names/dirs/assigns type nargs) (vl-gatetype-names/dirs/assigns type nargs-equiv))) :rule-classes :congruence)