Make a basic binary gate instance, e.g., an AND, OR, XOR, NAND, NOR, or XNOR gate.
(vl-make-binary-gateinst type out a b &key atts (loc '*vl-fakeloc*)) → inst
Function:
(defun vl-make-binary-gateinst-fn (type out a b atts loc) (declare (xargs :guard (and (vl-gatetype-p type) (vl-expr-p out) (vl-expr-p a) (vl-expr-p b) (vl-atts-p atts) (vl-location-p loc)))) (declare (xargs :guard (member-eq type (list :vl-and :vl-nand :vl-nor :vl-or :vl-xor :vl-xnor)))) (let ((__function__ 'vl-make-binary-gateinst)) (declare (ignorable __function__)) (prog2$ (or (and (equal (vl-expr->finalwidth out) 1) (equal (vl-expr->finalwidth a) 1) (equal (vl-expr->finalwidth b) 1)) (raise "Expected expressions of width 1.")) (make-vl-gateinst :type type :args (list (make-vl-plainarg :expr (vl-expr-fix out) :dir :vl-output) (make-vl-plainarg :expr (vl-expr-fix a) :dir :vl-input) (make-vl-plainarg :expr (vl-expr-fix b) :dir :vl-input)) :atts atts :loc loc))))
Theorem:
(defthm vl-gateinst-p-of-vl-make-binary-gateinst (b* ((inst (vl-make-binary-gateinst-fn type out a b atts loc))) (vl-gateinst-p inst)) :rule-classes :rewrite)
Theorem:
(defthm vl-make-binary-gateinst-fn-of-vl-gatetype-fix-type (equal (vl-make-binary-gateinst-fn (vl-gatetype-fix type) out a b atts loc) (vl-make-binary-gateinst-fn type out a b atts loc)))
Theorem:
(defthm vl-make-binary-gateinst-fn-vl-gatetype-equiv-congruence-on-type (implies (vl-gatetype-equiv type type-equiv) (equal (vl-make-binary-gateinst-fn type out a b atts loc) (vl-make-binary-gateinst-fn type-equiv out a b atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-binary-gateinst-fn-of-vl-expr-fix-out (equal (vl-make-binary-gateinst-fn type (vl-expr-fix out) a b atts loc) (vl-make-binary-gateinst-fn type out a b atts loc)))
Theorem:
(defthm vl-make-binary-gateinst-fn-vl-expr-equiv-congruence-on-out (implies (vl-expr-equiv out out-equiv) (equal (vl-make-binary-gateinst-fn type out a b atts loc) (vl-make-binary-gateinst-fn type out-equiv a b atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-binary-gateinst-fn-of-vl-expr-fix-a (equal (vl-make-binary-gateinst-fn type out (vl-expr-fix a) b atts loc) (vl-make-binary-gateinst-fn type out a b atts loc)))
Theorem:
(defthm vl-make-binary-gateinst-fn-vl-expr-equiv-congruence-on-a (implies (vl-expr-equiv a a-equiv) (equal (vl-make-binary-gateinst-fn type out a b atts loc) (vl-make-binary-gateinst-fn type out a-equiv b atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-binary-gateinst-fn-of-vl-expr-fix-b (equal (vl-make-binary-gateinst-fn type out a (vl-expr-fix b) atts loc) (vl-make-binary-gateinst-fn type out a b atts loc)))
Theorem:
(defthm vl-make-binary-gateinst-fn-vl-expr-equiv-congruence-on-b (implies (vl-expr-equiv b b-equiv) (equal (vl-make-binary-gateinst-fn type out a b atts loc) (vl-make-binary-gateinst-fn type out a b-equiv atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-binary-gateinst-fn-of-vl-atts-fix-atts (equal (vl-make-binary-gateinst-fn type out a b (vl-atts-fix atts) loc) (vl-make-binary-gateinst-fn type out a b atts loc)))
Theorem:
(defthm vl-make-binary-gateinst-fn-vl-atts-equiv-congruence-on-atts (implies (vl-atts-equiv atts atts-equiv) (equal (vl-make-binary-gateinst-fn type out a b atts loc) (vl-make-binary-gateinst-fn type out a b atts-equiv loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-binary-gateinst-fn-of-vl-location-fix-loc (equal (vl-make-binary-gateinst-fn type out a b atts (vl-location-fix loc)) (vl-make-binary-gateinst-fn type out a b atts loc)))
Theorem:
(defthm vl-make-binary-gateinst-fn-vl-location-equiv-congruence-on-loc (implies (vl-location-equiv loc loc-equiv) (equal (vl-make-binary-gateinst-fn type out a b atts loc) (vl-make-binary-gateinst-fn type out a b atts loc-equiv))) :rule-classes :congruence)