• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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-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
  • Transforms

Occform

Transform assignments into occurrences.

We now introduce routines to transform post-split assignments into occurrences of new, primitive modules.

We expect to see assignments of the form:

assign LVALUE = EXPR ;

where EXPR consists either of a single operand or of a single operation applied to operands. We expect to not encounter certain operators such as == and || which are handled by oprewrite.

We typically replace each assignment with an instance of a newly-generated module. For instance, if our operation is a + b, where the operation is being done in n bits, we introduce a new VL_N_BIT_PLUS module, and replace the assignment with an instance of this module.

Each of our -occform functions takes as arguments:

  • x, an assignment that typically must be of some particular form,
  • nf, a vl-namefactory-p to use when generating new names, and
  • warnings, an ordinary warnings accumulator.

And returns (mv new-warnings new-modules new-modinsts new-nf), where:

  • new-warnings is the new warnings accumulator which has been extended with any warnings,
  • new-modules are any newly generated modules that need to be added so that we can instantiate them---that is, this list will define modules like VL_13_BIT_PLUS that will be used to replace this assignment,
  • new-modinsts and new-assigns are any new module instances and assignments that, taken together, can replace x, and
  • new-nf is the updated vl-namefactory-p that is used to generate module instance names.

Typically new-assigns will be empty on success, and will just be (list x) on failure.

Subtopics

Vl-mux-occform
Transform an assignment of a conditional expression into occurrences.
Vl-basic-binary-op-occform
Transform an assignment of a basic binary operation into occurrences.
Vl-occform-mkports
Helper function for creating lists of port declarations.
Vl-unary-reduction-op-occform
Transform an assignment of a reduction operation into an equivalent module instance.
Vl-make-n-bit-mux
Generate a wide multiplexor module.
Vl-bitselect-occform
Transform assign lhs = foo[i] into occurrences (dynamic bitselects only!).
Vl-assign-occform
Transform an arbitrary single assignment into occurrences.
Vl-plusminus-occform
Transform an assignment of a addition/subtraction into occurrences.
Vl-shift-occform
Transform an assignment of a shift expression into occurrences.
Vl-gte-occform
Transform assign lhs = a > b into occurrences.
Vl-plain-occform
Transform a plain assignment into occurrences.
Vl-unary-not-occform
Transform assign lhs = ~a into occurrences.
Vl-rem-occform
Transform assign lhs = a % b into occurrences.
Vl-div-occform
Transform assign lhs = a / b into occurrences.
Vl-ceq-occform
Transform an assignment of a === expression into occurrences.
Vl-mult-occform
Transform assign lhs = a * b into occurrences.
Vl-make-n-bit-dynamic-bitselect-m
Generate a dynamic bit-selection module for an N bit wire and an M bit select.
Vl-simple-instantiate
Convenient way to generating module instances.
Vl-occform-mkwires
Helper function for creating lists of net declarations.
Vl-assignlist-occform
Project vl-assign-occform across a list of assignments.
Vl-occform-argfix
Make extensions explicit for arguments to occform modules.
Vl-make-n-bit-unsigned-gte
Generate an unsigned greater-than or equal comparison module.
Vl-make-2^n-bit-dynamic-bitselect
Generates a dynamic bit-selection module for wire widths that are powers of 2.
Vl-make-n-bit-div-rem
Top-level division/remainder module.
Vl-make-n-bit-plusminus
Generate an addition or subtraction module.
Vl-make-n-bit-signed-gte
Generate a signed greater-than or equal comparison module.
Vl-make-n-bit-shr-by-m-bits
Generate a module that shifts an N bit number right by an M bit number.
Vl-make-n-bit-shl-by-m-bits
Generate a module that shifts an N bit number left by an M bit number.
Vl-occform-mkport
Helper for creating ports in generated modules.
Vl-make-n-bit-dynamic-bitselect
Generate a basic dynamic bit-selection module.
Vl-make-n-bit-reduction-op
Generate a wide reduction AND, OR, or XOR module.
Vl-make-n-bit-adder-core
Generate an N-bit basic ripple-carry adder module.
Vl-make-n-bit-xdetect
Generate a module that detects X/Z bits.
Vl-make-n-bit-x-propagator
Generate a module that propagates Xes from inputs into an answer.
Vl-make-n-bit-shl-place-p
Generate a module that conditionally shifts an N bit number by 2**(P-1) bits to the left.
Vl-make-n-bit-shr-place-p
Generate a module that conditionally shifts an N bit number by 2**(P-1) bits to the right.
Vl-make-n-bit-mult
Generate an multiplier module.
Vl-occform-mkwire
Helper function for creating ports in generated modules.
Vl-make-nedgeflop-vec
Generate a w-bit wide, n-edge flop with output delay d
Vl-make-n-bit-binary-op
Generate a wide, pointwise AND, OR, XOR, or XNOR module.
Vl-make-list-of-netdecls
Generate a list of distinct wires with a particular range.
Vl-make-n-bit-delay-1
Generate an n-bit wide, 1-tick delay module.
Vl-make-n-bit-zmux
Generate a wide tri-state buffer module.
*vl-2-bit-dynamic-bitselect*
Primitive dynamic bit-selection module.
Vl-make-n-bit-unsigned-rem
Generate an unsigned remainder module.
Vl-make-n-bit-unsigned-div
Generate an unsigned divider module.
Vl-make-n-bit-shr-place-ps
Generate a list of place-shifters, counting down from P to 1.
Vl-make-n-bit-shl-place-ps
Generate a list of place-shifters, counting down from P to 1.
Vl-make-n-bit-assign
Generate a wide assignment module.
Vl-make-n-bit-x
Generate a wide X module.
Vl-make-n-bit-ceq
Generate a wide case-equality module.
Vl-make-n-bit-xor-each
Generate a module that XORs a bit with each bit of a vector.
Vl-make-n-bit-not
Generate a wide negation module.
Vl-make-1-bit-delay-m
Generate a one-bit wide, M-tick delay module.
Vl-make-n-bit-delay-m
Generate an N-bit wide, M-tick delay module.
*vl-1-bit-signed-gte*
Degenerate, single-bit signed greater-than-or-equal module.
*vl-1-bit-div-rem*
One-bit division and remainder.
*vl-1-bit-adder-core*
Primitive one-bit full-adder module.
Vl-make-nedgeflop
Generate an N-bit register with K edges.
*vl-1-bit-mult*
One-bit multiplier.
*vl-1-bit-dynamic-bitselect*
Degenerate 1-bit dynamic bit-selection module.