		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-make-n-bit-plusminus

Generate an addition or subtraction module.

Signature
(vl-make-n-bit-plusminus type n) → mods
Arguments: type — Guard (member type (list :vl-binary-plus :vl-binary-minus)).; 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).

Depending on the type, which should be either :vl-binary-plus or :vl-binary-minus, we generate a gate-based addition or subtraction module that is semantically equivalent to:

module VL_N_BIT_{PLUS,MINUS} (out, a, b) ;
  output [n-1:0] out;
  input [n-1:0] a;
  input [n-1:0] b;

// One of:

  assign out = a + b;  // For PLUS
  assign out = a - b;  // For MINUS

endmodule

These modules capture the behavior specified by Verilog for addition and subtraction, including the requirement that if any bit of a or b is X/Z then the entire output is entirely X.

We basically combine a simple ripple-carry adder with some additional X-detection and propagation circuitry. This makes our adder rather bulky and unlike the actual hardware that would probably be synthesized or implemented.

Definitions and Theorems

Function: vl-make-n-bit-plusminus

(defun vl-make-n-bit-plusminus (type n)
 (declare
   (xargs
        :guard (and (member type
                            (list :vl-binary-plus :vl-binary-minus))
                    (posp n))))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-make-n-bit-plusminus))
  (declare (ignorable __function__))
  (b*
   ((n (lposfix n))
    (name (hons-copy (cat "VL_" (natstr n)
                          "_BIT_"
                          (case type (:vl-binary-plus "PLUS")
                                (:vl-binary-minus "MINUS")))))
    ((mv out-expr
         out-port out-portdecl out-vardecl)
     (vl-occform-mkport "out" :vl-output n))
    ((mv a-expr a-port a-portdecl a-vardecl)
     (vl-occform-mkport "a" :vl-input n))
    ((mv b-expr b-port b-portdecl b-vardecl)
     (vl-occform-mkport "b" :vl-input n))
    ((mv sum-expr sum-vardecl)
     (vl-occform-mkwire "sum" n))
    ((mv carry-expr carry-vardecl)
     (vl-primitive-mkwire "carry"))
    ((mv cin bin
         sub-vardecls sub-modinsts sub-support)
     (if (eq type :vl-binary-plus)
         (mv |*sized-1'b0*| b-expr nil nil nil)
       (b*
        (((mv bnot-expr bnot-vardecl)
          (vl-occform-mkwire "bnot" n))
         ((cons bnot-mod bnot-support)
          (vl-make-n-bit-not n))
         (bnot-inst
              (vl-simple-inst bnot-mod "mk_bnot" bnot-expr b-expr)))
        (mv |*sized-1'b1*|
            bnot-expr (list bnot-vardecl)
            (list bnot-inst)
            (cons bnot-mod bnot-support)))))
    ((cons core-mod core-support)
     (vl-make-n-bit-adder-core n))
    (core-inst (vl-simple-inst core-mod "core"
                               sum-expr carry-expr a-expr bin cin))
    ((cons xprop-mod xprop-support)
     (vl-make-n-bit-x-propagator n n))
    (xprop-inst (vl-simple-inst xprop-mod "xprop"
                                out-expr sum-expr a-expr b-expr)))
   (list*
       (make-vl-module
            :name name
            :origname name
            :ports (list out-port a-port b-port)
            :portdecls (list out-portdecl a-portdecl b-portdecl)
            :vardecls (list* out-vardecl a-vardecl b-vardecl
                             sum-vardecl carry-vardecl sub-vardecls)
            :modinsts (append sub-modinsts
                              (list core-inst xprop-inst))
            :minloc *vl-fakeloc*
            :maxloc *vl-fakeloc*)
       core-mod xprop-mod
       (append sub-support
               core-support xprop-support)))))

Theorem: vl-modulelist-p-of-vl-make-n-bit-plusminus

(defthm vl-modulelist-p-of-vl-make-n-bit-plusminus
  (b* ((mods (vl-make-n-bit-plusminus type n)))
    (vl-modulelist-p mods))
  :rule-classes :rewrite)

Theorem: type-of-vl-make-n-bit-plusminus

(defthm type-of-vl-make-n-bit-plusminus
  (and (true-listp (vl-make-n-bit-plusminus type n))
       (consp (vl-make-n-bit-plusminus type n)))
  :rule-classes :type-prescription)

Theorem: vl-make-n-bit-plusminus-of-pos-fix-n

(defthm vl-make-n-bit-plusminus-of-pos-fix-n
  (equal (vl-make-n-bit-plusminus type (pos-fix n))
         (vl-make-n-bit-plusminus type n)))

Theorem: vl-make-n-bit-plusminus-pos-equiv-congruence-on-n

(defthm vl-make-n-bit-plusminus-pos-equiv-congruence-on-n
  (implies (acl2::pos-equiv n n-equiv)
           (equal (vl-make-n-bit-plusminus type n)
                  (vl-make-n-bit-plusminus type n-equiv)))
  :rule-classes :congruence)