		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-xdetect

Generate a module that detects X/Z bits.

Signature
(vl-make-n-bit-xdetect n) → mods
Arguments: n — Guard (posp n).
Returns: mods — A non-empty module list. The first module in the list is the desired module; the other modules are any necessary supporting modules.
Type (vl-modulelist-p 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 out to X whenever any bit of in is X or Z. Otherwise, we set out to 0.

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 VL_N_BIT_XDETECT to see if any input bit is X or Z, then XOR the output bit with every bit of the answer from a compare, addition, subtraction, etc. If the X-DET bit is zero, then XOR'ing it with the answer just yields the original answer. But if it is X, then the resulting bits are all X.

Definitions and Theorems

Function: vl-make-n-bit-xdetect

(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: vl-modulelist-p-of-vl-make-n-bit-xdetect

(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: type-of-vl-make-n-bit-xdetect

(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: vl-make-n-bit-xdetect-of-pos-fix-n

(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: vl-make-n-bit-xdetect-pos-equiv-congruence-on-n

(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)