Wrap an input to a gate instance in a truncation expression.
(vl-fixup-wide-gate-input in) → fixed-in
Consider an AND gate with wide inputs like this:
wire out; wire [1:0] in1, in2; and(out, in1, in2);
NCV and VCS complain if the output is more than a single bit, but they accept wide inputs. They also behave in different ways in this case: NCV does a reduction or on the input, while VCS truncates it and just operates on the bottom bit.
Here we mimic VCS's behavior, wrapping each input expression
Function:
(defun vl-fixup-wide-gate-input (in) (declare (xargs :guard (sv::svex-p in))) (let ((__function__ 'vl-fixup-wide-gate-input)) (declare (ignorable __function__)) (sv::svcall sv::zerox (sv::make-svex-quote :val 1) in)))
Theorem:
(defthm svex-p-of-vl-fixup-wide-gate-input (b* ((fixed-in (vl-fixup-wide-gate-input in))) (sv::svex-p fixed-in)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-fixup-wide-gate-input (b* ((?fixed-in (vl-fixup-wide-gate-input in))) (implies (not (member v (sv::svex-vars in))) (not (member v (sv::svex-vars fixed-in))))))
Theorem:
(defthm vl-fixup-wide-gate-input-of-svex-fix-in (equal (vl-fixup-wide-gate-input (sv::svex-fix in)) (vl-fixup-wide-gate-input in)))
Theorem:
(defthm vl-fixup-wide-gate-input-svex-equiv-congruence-on-in (implies (sv::svex-equiv in in-equiv) (equal (vl-fixup-wide-gate-input in) (vl-fixup-wide-gate-input in-equiv))) :rule-classes :congruence)