• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
          • Expression-sizing
          • Occform
            • Vl-mux-occform
            • Vl-basic-binary-op-occform
            • Vl-occform-mkports
            • Vl-unary-reduction-op-occform
            • Vl-make-n-bit-mux
            • Vl-bitselect-occform
            • Vl-assign-occform
            • Vl-plusminus-occform
            • Vl-shift-occform
            • Vl-gte-occform
            • Vl-plain-occform
            • Vl-unary-not-occform
            • Vl-rem-occform
            • Vl-div-occform
            • Vl-ceq-occform
            • Vl-mult-occform
            • Vl-make-n-bit-dynamic-bitselect-m
            • Vl-simple-instantiate
            • Vl-occform-mkwires
            • Vl-assignlist-occform
            • Vl-occform-argfix
            • Vl-make-n-bit-unsigned-gte
            • Vl-make-2^n-bit-dynamic-bitselect
            • Vl-make-n-bit-div-rem
            • Vl-make-n-bit-plusminus
            • Vl-make-n-bit-signed-gte
            • Vl-make-n-bit-shr-by-m-bits
            • Vl-make-n-bit-shl-by-m-bits
            • Vl-occform-mkport
            • Vl-make-n-bit-dynamic-bitselect
            • Vl-make-n-bit-reduction-op
            • Vl-make-n-bit-adder-core
            • Vl-make-n-bit-xdetect
            • Vl-make-n-bit-x-propagator
            • Vl-make-n-bit-shl-place-p
            • Vl-make-n-bit-shr-place-p
            • Vl-make-n-bit-mult
            • Vl-occform-mkwire
            • Vl-make-nedgeflop-vec
            • Vl-make-n-bit-binary-op
            • Vl-make-list-of-netdecls
            • Vl-make-n-bit-delay-1
            • Vl-make-n-bit-zmux
            • *vl-2-bit-dynamic-bitselect*
            • Vl-make-n-bit-unsigned-rem
            • Vl-make-n-bit-unsigned-div
            • Vl-make-n-bit-shr-place-ps
            • Vl-make-n-bit-shl-place-ps
            • Vl-make-n-bit-assign
            • Vl-make-n-bit-x
            • Vl-make-n-bit-ceq
            • Vl-make-n-bit-xor-each
            • Vl-make-n-bit-not
            • Vl-make-1-bit-delay-m
            • Vl-make-n-bit-delay-m
            • *vl-1-bit-signed-gte*
            • *vl-1-bit-div-rem*
            • *vl-1-bit-adder-core*
              • *vl-1-bit-adder-core-support*
            • Vl-make-nedgeflop
            • *vl-1-bit-mult*
            • *vl-1-bit-dynamic-bitselect*
          • Oprewrite
          • Expand-functions
          • Delayredux
          • Unparameterization
          • Caseelim
          • Split
          • Selresolve
          • Weirdint-elim
          • Vl-delta
          • Replicate-insts
          • Rangeresolve
          • Propagate
          • Clean-selects
          • Clean-params
          • Blankargs
          • Inline-mods
          • Expr-simp
          • Trunc
          • Always-top
          • Gatesplit
          • Gate-elim
          • Expression-optimization
          • Elim-supplies
          • Wildelim
          • Drop-blankports
          • Clean-warnings
          • Addinstnames
          • Custom-transform-hooks
          • Annotate
          • Latchcode
          • Elim-unused-vars
          • Problem-modules
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Occform

*vl-1-bit-adder-core*

Primitive one-bit full-adder module.

A full-adder is a one-bit adder that produces a sum and carry. We use the following definition:

module VL_1_BIT_ADDER_CORE (sum, cout, a, b, cin) ;
  output sum, cout;
  input a, b, cin;
  wire t1, t2, t3;

  assign t1 = a ^ b;
  assign sum = t1 ^ cin;
  assign t2 = t1 & cin;
  assign t3 = a & b;
  assign cout = t2 | t3;

endmodule

This is only a "core." It doesn't quite correspond to an addition like assign {carry, sum} = a + b + cin in Verilog because of X handling. See vl-make-n-bit-plusminus for the real module generator.

Definition: *vl-1-bit-adder-core*

(defconst *vl-1-bit-adder-core*
 (b*
  ((name (hons-copy "VL_1_BIT_ADDER_CORE"))
   ((mv sum-expr
        sum-port sum-portdecl sum-vardecl)
    (vl-primitive-mkport "sum" :vl-output))
   ((mv cout-expr
        cout-port cout-portdecl cout-vardecl)
    (vl-primitive-mkport "cout" :vl-output))
   ((mv a-expr a-port a-portdecl a-vardecl)
    (vl-primitive-mkport "a" :vl-input))
   ((mv b-expr b-port b-portdecl b-vardecl)
    (vl-primitive-mkport "b" :vl-input))
   ((mv cin-expr
        cin-port cin-portdecl cin-vardecl)
    (vl-primitive-mkport "cin" :vl-input))
   ((mv t1-expr t1-vardecl)
    (vl-primitive-mkwire "t1"))
   ((mv t2-expr t2-vardecl)
    (vl-primitive-mkwire "t2"))
   ((mv t3-expr t3-vardecl)
    (vl-primitive-mkwire "t3"))
   (t1-inst (vl-simple-inst *vl-1-bit-xor*
                            "mk_t1" t1-expr a-expr b-expr))
   (sum-inst (vl-simple-inst *vl-1-bit-xor*
                             "mk_sum" sum-expr t1-expr cin-expr))
   (t2-inst (vl-simple-inst *vl-1-bit-and*
                            "mk_t2" t2-expr t1-expr cin-expr))
   (t3-inst (vl-simple-inst *vl-1-bit-and*
                            "mk_t3" t3-expr a-expr b-expr))
   (cout-inst (vl-simple-inst *vl-1-bit-or*
                              "mk_cout" cout-expr t2-expr t3-expr)))
  (hons-copy
       (make-vl-module
            :name name
            :origname name
            :ports (list sum-port
                         cout-port a-port b-port cin-port)
            :portdecls (list sum-portdecl cout-portdecl
                             a-portdecl b-portdecl cin-portdecl)
            :vardecls (list sum-vardecl cout-vardecl
                            a-vardecl b-vardecl cin-vardecl
                            t1-vardecl t2-vardecl t3-vardecl)
            :modinsts (list t1-inst
                            sum-inst t2-inst t3-inst cout-inst)
            :minloc *vl-fakeloc*
            :maxloc *vl-fakeloc*))))

Subtopics

*vl-1-bit-adder-core-support*