Make a unary (buf or not) gate instance.
(vl-make-unary-gateinst type out in &key atts (loc '*vl-fakeloc*)) → inst
Function:
(defun vl-make-unary-gateinst-fn (type out in atts loc) (declare (xargs :guard (and (vl-gatetype-p type) (vl-expr-p out) (vl-expr-p in) (vl-atts-p atts) (vl-location-p loc)))) (declare (xargs :guard (member type (list :vl-buf :vl-not)))) (let ((__function__ 'vl-make-unary-gateinst)) (declare (ignorable __function__)) (progn$ (or (and (equal (vl-expr->finalwidth out) 1) (equal (vl-expr->finalwidth in) 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 in) :dir :vl-input)) :atts atts :loc loc))))
Theorem:
(defthm vl-gateinst-p-of-vl-make-unary-gateinst (b* ((inst (vl-make-unary-gateinst-fn type out in atts loc))) (vl-gateinst-p inst)) :rule-classes :rewrite)
Theorem:
(defthm vl-make-unary-gateinst-fn-of-vl-gatetype-fix-type (equal (vl-make-unary-gateinst-fn (vl-gatetype-fix type) out in atts loc) (vl-make-unary-gateinst-fn type out in atts loc)))
Theorem:
(defthm vl-make-unary-gateinst-fn-vl-gatetype-equiv-congruence-on-type (implies (vl-gatetype-equiv type type-equiv) (equal (vl-make-unary-gateinst-fn type out in atts loc) (vl-make-unary-gateinst-fn type-equiv out in atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-unary-gateinst-fn-of-vl-expr-fix-out (equal (vl-make-unary-gateinst-fn type (vl-expr-fix out) in atts loc) (vl-make-unary-gateinst-fn type out in atts loc)))
Theorem:
(defthm vl-make-unary-gateinst-fn-vl-expr-equiv-congruence-on-out (implies (vl-expr-equiv out out-equiv) (equal (vl-make-unary-gateinst-fn type out in atts loc) (vl-make-unary-gateinst-fn type out-equiv in atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-unary-gateinst-fn-of-vl-expr-fix-in (equal (vl-make-unary-gateinst-fn type out (vl-expr-fix in) atts loc) (vl-make-unary-gateinst-fn type out in atts loc)))
Theorem:
(defthm vl-make-unary-gateinst-fn-vl-expr-equiv-congruence-on-in (implies (vl-expr-equiv in in-equiv) (equal (vl-make-unary-gateinst-fn type out in atts loc) (vl-make-unary-gateinst-fn type out in-equiv atts loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-unary-gateinst-fn-of-vl-atts-fix-atts (equal (vl-make-unary-gateinst-fn type out in (vl-atts-fix atts) loc) (vl-make-unary-gateinst-fn type out in atts loc)))
Theorem:
(defthm vl-make-unary-gateinst-fn-vl-atts-equiv-congruence-on-atts (implies (vl-atts-equiv atts atts-equiv) (equal (vl-make-unary-gateinst-fn type out in atts loc) (vl-make-unary-gateinst-fn type out in atts-equiv loc))) :rule-classes :congruence)
Theorem:
(defthm vl-make-unary-gateinst-fn-of-vl-location-fix-loc (equal (vl-make-unary-gateinst-fn type out in atts (vl-location-fix loc)) (vl-make-unary-gateinst-fn type out in atts loc)))
Theorem:
(defthm vl-make-unary-gateinst-fn-vl-location-equiv-congruence-on-loc (implies (vl-location-equiv loc loc-equiv) (equal (vl-make-unary-gateinst-fn type out in atts loc) (vl-make-unary-gateinst-fn type out in atts loc-equiv))) :rule-classes :congruence)