• 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
          • Oprewrite
          • Expand-functions
          • Delayredux
          • Unparameterization
          • Caseelim
          • Split
          • Selresolve
          • Weirdint-elim
          • Vl-delta
            • Vl-delta-p
            • Vl-delta-fix
            • Make-vl-delta
            • Vl-delta-equiv
            • Change-vl-delta
            • Vl-delta->warnings
            • Vl-delta->vardecls
            • Vl-delta->modinsts
            • Vl-delta->gateinsts
            • Vl-delta->assigns
            • Vl-delta->addmods
            • Vl-delta->nf
          • 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

Vl-delta

A set of changes to be made to a module.

This is a product type introduced by defprod.

Fields
nf — vl-namefactory
vardecls — vl-vardecllist
assigns — vl-assignlist
modinsts — vl-modinstlist
gateinsts — vl-gateinstlist
warnings — vl-warninglist
addmods — vl-modulelist

An vl-delta-p is mostly just a bunch of accumulators of different types, which may be useful when writing a transform that makes updates to a module. It also has a vl-namefactory-p which can be used to generate fresh names.

What is this all about?

Many simple transforms just walk through a module's elements and rewrite them in some "local" way. For instance, to size expressions or resolve arguments, we're just walking over the existing module elements and annotating or changing them. These sorts of transforms usually have no need for a delta.

Deltas become useful when a transform needs to rewrite the module elements in some way that depends on other stuff being added to the module and/or to the module list. For example:

  • When we split up expressions, we might rewrite a + b into tmp, while also adding wire[3:0] tmp and assign tmp = a + b to the module.
  • When we turn expressions into occurrences, we might delete assign tmp = a + b altogether, while adding
    VL_4_BIT_PLUS _adder_123 (tmp, a, b)
    to the module and adding VL_4_BIT_PLUS and its supporting modules in the module list.

We found that writing these kinds of transforms meant passing around several different accumulators for the different types of elements we wanted to add. It is quite painful to write a whole set of functions that take, say, five accumulators, and to prove even the simple type theorems about them. A delta is mainly just a bundle of these accumulators, which greatly simplifies the code for transforms like split.

We found it useful to add a vl-namefactory-p to the delta, since that way any transform that wants to generate fresh names can do so easily.

Subtopics

Vl-delta-p
Recognizer for vl-delta structures.
Vl-delta-fix
Fixing function for vl-delta structures.
Make-vl-delta
Basic constructor macro for vl-delta structures.
Vl-delta-equiv
Basic equivalence relation for vl-delta structures.
Change-vl-delta
Modifying constructor for vl-delta structures.
Vl-delta->warnings
Get the warnings field from a vl-delta.
Vl-delta->vardecls
Get the vardecls field from a vl-delta.
Vl-delta->modinsts
Get the modinsts field from a vl-delta.
Vl-delta->gateinsts
Get the gateinsts field from a vl-delta.
Vl-delta->assigns
Get the assigns field from a vl-delta.
Vl-delta->addmods
Get the addmods field from a vl-delta.
Vl-delta->nf
Get the nf field from a vl-delta.