• 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
          • Replicate-insts
          • Rangeresolve
          • Propagate
          • Clean-selects
          • Clean-params
          • Blankargs
          • Inline-mods
          • Expr-simp
          • Trunc
          • Always-top
            • Edgesynth
            • Stmtrewrite
            • Cblock
            • Vl-always-convert-regports
            • Vl-always-convert-regs
            • Stmttemps
            • Edgesplit
            • Vl-always-check-reg
            • Vl-convert-regs
            • Latchsynth
              • Vl-module-latchsynth
              • Vl-modulelist-latchsynth-aux
              • Vl-modulelist-latchsynth
              • Vl-design-latchsynth
            • Vl-always-check-regs
            • Vl-match-always-at-some-edges
            • Unelse
            • Vl-always-convert-reg
            • Vl-design-always-backend
            • Vl-stmt-guts
            • Vl-always-convert-regport
            • Vl-always-scary-regs
            • Eliminitial
            • Ifmerge
            • Vl-edge-control-p
            • Elimalways
          • 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
  • Always-top

Latchsynth

Main transform for synthesizing simple latch-like always blocks into instances of primitive latch modules.

This is a sort of back-end transform that does the final conversion of already-simplified always statements into latches. This is quite similar to how the occform transform converts Verilog expressions into explicit instances of generated modules, except that here we are converting always statements into instances of latch modules.

Notes:

  • We support only a very small set of always statements here; see latchcode. Typically you will want to run other statement-simplifying transformations first to get them into this form; see always-top.
  • We expect expressions to be sized so that we can tell which sizes of latch modules to introduce.
  • We expect modules to be free of initial statements, otherwise we could produce invalid modules when we convert registers into nets.
  • This is a best-effort style transform which will leave unsupported always blocks alone. We usually follow up with elimalways to throw out (with fatal warnings) modules whose always blocks were not supported.

Subtopics

Vl-module-latchsynth
Synthesize simple latch-like always blocks in a module.
Vl-modulelist-latchsynth-aux
Vl-modulelist-latchsynth
Synthesize latch-like always blocks in a module list, perhaps adding some new, supporting modules.
Vl-design-latchsynth
Top-level latchsynth transform.