• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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-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-make-n-bit-assign

    Generate a wide assignment module.

    Signature
    (vl-make-n-bit-assign 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 module that is semantically equal to:

    module VL_N_BIT_ASSIGN (out, in) ;
      output [n-1:0] out;
      input [n-1:0] in;
      assign out = in;
    endmodule

    We actually implement these modules using a list of *vl-1-bit-assign* instances, one for each bit. For instance, we implement our four-bit assignment module as:

    module VL_4_BIT_ASSIGN (out, in);
      output [3:0] out ;
      input [3:0] in ;
      VL_1_BIT_ASSIGN bit_0 (out[0], in[0]) ;
      VL_1_BIT_ASSIGN bit_1 (out[1], in[1]) ;
      VL_1_BIT_ASSIGN bit_2 (out[2], in[2]) ;
      VL_1_BIT_ASSIGN bit_3 (out[3], in[3]) ;
    endmodule

    Definitions and Theorems

    Function: vl-make-n-bit-assign

    (defun vl-make-n-bit-assign (n)
     (declare (xargs :guard (posp n)))
     (declare (xargs :guard t))
     (let ((__function__ 'vl-make-n-bit-assign))
      (declare (ignorable __function__))
      (b* ((n (lposfix n))
           ((when (eql n 1))
            (list *vl-1-bit-assign*))
           (name (hons-copy (cat "VL_" (natstr n) "_BIT_ASSIGN")))
           ((mv out-expr
                out-port out-portdecl out-vardecl)
            (vl-occform-mkport "out" :vl-output n))
           ((mv in-expr in-port in-portdecl in-vardecl)
            (vl-occform-mkport "in" :vl-input n))
           (out-wires (vl-make-list-of-bitselects out-expr 0 (- n 1)))
           (in-wires (vl-make-list-of-bitselects in-expr 0 (- n 1)))
           (modinsts (vl-simple-inst-list *vl-1-bit-assign*
                                          "bit" out-wires in-wires)))
        (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 modinsts
                              :minloc *vl-fakeloc*
                              :maxloc *vl-fakeloc*)
              *vl-1-bit-assign*))))

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

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

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

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

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

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

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

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