• 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
              • Vl-modulelist-stmtrewrite
              • Vl-blockstmt-rewrite
              • Vl-repeatstmt-rewrite
              • Vl-flatten-blocks
              • Vl-stmt-rewrite-top
              • Vl-casestmt-rewrite
              • Vl-stmt-rewrite
              • Vl-waitstmt-rewrite
              • Vl-ifstmt-combine-rewrite
              • Vl-forstmt-rewrite
              • Vl-initiallist-stmtrewrite
              • Vl-alwayslist-stmtrewrite
              • Vl-initial-stmtrewrite
              • Vl-foreverstmt-rewrite
              • Vl-always-stmtrewrite
              • Vl-module-stmtrewrite
              • Vl-design-stmtrewrite
              • Vl-remove-null-statements
              • Vl-$vcover-stmt-p
              • Vl-$display-stmt-p
              • Vl-caselist-all-null-p
            • Cblock
            • Vl-always-convert-regports
            • Vl-always-convert-regs
            • Stmttemps
            • Edgesplit
            • Vl-always-check-reg
            • Vl-convert-regs
            • 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

Stmtrewrite

Rewrite statements into simpler forms.

This transform simplifies Verilog statements by applying rewrite rules. The idea is to make later statement processing simpler by reducing the variety of statements that need to be supported. This is somewhat similar to how the oprewrite transform eliminates certain operators, leaving us with fewer operators to support later on. See always-top for how this fits into our overall handling of always blocks.

Note that, for instance, our rewrites eliminate $display statements. This is suitable when your goal is to analyze the functionality of the module from a synthesis/build perspective, e.g., with esim. But it is obviously not suitable if you want to use the resulting modules with a Verilog simulator.

Notes:

  • This transform should typically be run after unparameterization so that, e.g., width parameters will have been propagated. For instance, things like repeat (n) body won't get unrolled unless n has already been resolved.
  • It should typically run before sizing, since we generate unsized expressions.

Some implemented rewrites include:

  • $display(...) → null
  • pure-null if/case stmts → null
  • eliminate null stmts from blocks
  • empty blocks → null
  • collapse singleton blocks (i.e., begin stmt end --> stmt)
  • flatten compatible sub-blocks
  • @(...) null → null (top level only)
  • merge nested ifs (without elses)
  • wait statements → while loops
  • forever statements → while loops
  • unroll some repeat statements (up to a limit)
  • eliminate always null;
  • eliminate initial null;
  • eliminate for(...) null;

Note that we don't transform case statements into if statement here, but that's done in caseelim.

Bozo eventually we should also unroll simple while/for loops.

Subtopics

Vl-modulelist-stmtrewrite
(vl-modulelist-stmtrewrite x unroll-limit) maps vl-module-stmtrewrite across a list.
Vl-blockstmt-rewrite
Flatten sub-blocks, eliminate unnecessary blocks, and remove any null statements from a block.
Vl-repeatstmt-rewrite
Unroll deterministic repeat statements.
Vl-flatten-blocks
Collapse nested begin/end and fork/join blocks.
Vl-stmt-rewrite-top
Wrapper for vl-stmt-rewrite that adds additional rewrites that are valid only for top-level statements.
Vl-casestmt-rewrite
Eliminate pure-null case statements.
Vl-stmt-rewrite
Core statement rewriter.
Vl-waitstmt-rewrite
Convert wait statements into empty while loops.
Vl-ifstmt-combine-rewrite
Eliminate pure-null if statements and merge simply nested ifs.
Vl-forstmt-rewrite
Eliminate purely null vl-forstmts.
Vl-initiallist-stmtrewrite
Vl-alwayslist-stmtrewrite
Vl-initial-stmtrewrite
Vl-foreverstmt-rewrite
Convert forever statements into while loops.
Vl-always-stmtrewrite
Vl-module-stmtrewrite
Vl-design-stmtrewrite
Top-level stmtrewrite transform.
Vl-remove-null-statements
Vl-$vcover-stmt-p
BOZO Centaur specific.
Vl-$display-stmt-p
Recognize a $display statement.
Vl-caselist-all-null-p