Generate a module that detects X/Z bits.
(vl-make-n-bit-xdetect n) → mods
We generate a gate-based module with the following signature:
module VL_N_BIT_XDETECT (out, in) ; output out; input [n-1:0] in; ... endmodule
We set
This module is useful because many of Verilog's arithmetic
expressions (compares, additions, subtractions, etc.) require that if any input
bit is X or Z, then the entire output should be X. The basic idea is to use
Function:
(defun vl-make-n-bit-xdetect (n) (declare (xargs :guard (posp n))) (declare (xargs :guard t)) (let ((__function__ 'vl-make-n-bit-xdetect)) (declare (ignorable __function__)) (b* ((n (lposfix n)) (name (hons-copy (cat "VL_" (natstr n) "_BIT_X_DETECT"))) ((mv out-expr out-port out-portdecl out-vardecl) (vl-occform-mkport "out" :vl-output 1)) ((mv in-expr in-port in-portdecl in-vardecl) (vl-occform-mkport "in" :vl-input n)) ((when (eql n 1)) (let ((out-inst (vl-simple-inst *vl-1-bit-xor* "ans" out-expr in-expr in-expr))) (list (make-vl-module :name name :origname name :ports (list out-port in-port) :portdecls (list out-portdecl in-portdecl) :vardecls (list out-vardecl in-vardecl) :modinsts (list out-inst) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) *vl-1-bit-xor*))) ((mv temp-expr temp-vardecl) (vl-occform-mkwire "temp" 1)) ((cons temp-mod temp-support) (vl-make-n-bit-reduction-op :vl-unary-xor n)) (temp-inst (vl-simple-inst temp-mod "mk_temp" temp-expr in-expr)) (out-inst (vl-simple-inst *vl-1-bit-xor* "mk_out" out-expr temp-expr temp-expr))) (list* (make-vl-module :name name :origname name :ports (list out-port in-port) :portdecls (list out-portdecl in-portdecl) :vardecls (list out-vardecl in-vardecl temp-vardecl) :modinsts (list temp-inst out-inst) :minloc *vl-fakeloc* :maxloc *vl-fakeloc*) temp-mod temp-support))))
Theorem:
(defthm vl-modulelist-p-of-vl-make-n-bit-xdetect (b* ((mods (vl-make-n-bit-xdetect n))) (vl-modulelist-p mods)) :rule-classes :rewrite)
Theorem:
(defthm type-of-vl-make-n-bit-xdetect (and (true-listp (vl-make-n-bit-xdetect n)) (consp (vl-make-n-bit-xdetect n))) :rule-classes :type-prescription)
Theorem:
(defthm vl-make-n-bit-xdetect-of-pos-fix-n (equal (vl-make-n-bit-xdetect (pos-fix n)) (vl-make-n-bit-xdetect n)))
Theorem:
(defthm vl-make-n-bit-xdetect-pos-equiv-congruence-on-n (implies (acl2::pos-equiv n n-equiv) (equal (vl-make-n-bit-xdetect n) (vl-make-n-bit-xdetect n-equiv))) :rule-classes :congruence)