• 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-edgesplitstmt-p
              • Vl-edgesplit-make-new-alwayses
              • Vl-modulelist-edgesplit
              • Vl-edgesplit-make-new-always
              • Vl-alwayslist-edgesplit
              • Vl-edgesplit-atomicstmt-for-lvalue
              • Vl-edgesplit-stmt-for-lvalue
              • Vl-always-edgesplit
              • Vl-edgesplitstmt-lvalues
              • Vl-edgesplit-atomicstmt-lvalues
              • Vl-module-edgesplit
              • Vl-edgesplit-atomicstmt-p
              • Vl-design-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

Edgesplit

Split up edge-triggered always blocks that write to multiple registers.

Our goal here is to reduce always blocks that write to several different registers. We only try to support always blocks with:

  • Edge-triggered sensitivity lists,
  • Non-blocking assignments to whole identifiers,
  • If/then/else statements,
  • Begin/end blocks.

For instance, a suitable block might be:

always @(posedge clk or posedge reset)
  begin
    q1 <= d1;
    if (reset)
       q2 <= 0;
    else
       q2 <= d2;
  end

We could split this block up into two always blocks:

always @(posedge clk or posedge reset)
   q1 <= d1;

always @(posedge clk or posedge reset)
   if (reset)
      q2 <= 0;
   else
      q2 <= d2;

This is just a generally nice simplification that lets us only consider a single register at a time.

BOZO we currently allow always blocks to be split up even if the assignments have different delays. This seems okay. But it would be good to explore this more and try to understand whether it's truly reasonable.

Subtopics

Vl-edgesplitstmt-p
Recognize statements that are simple enough for us to split up.
Vl-edgesplit-make-new-alwayses
(vl-edgesplit-make-new-alwayses x ctrl body atts loc) maps vl-edgesplit-make-new-always across a list.
Vl-modulelist-edgesplit
(vl-modulelist-edgesplit x) maps vl-module-edgesplit across a list.
Vl-edgesplit-make-new-always
Create the new, split up always blocks for a single lvalue.
Vl-alwayslist-edgesplit
(vl-alwayslist-edgesplit x) applies vl-always-edgesplit to every member of the list x, and appends together all the resulting lists.
Vl-edgesplit-atomicstmt-for-lvalue
Determine an atomic, splittable statement's effect on a single lvalue.
Vl-edgesplit-stmt-for-lvalue
Determine a splittable statement's effect on a single lvalue.
Vl-always-edgesplit
Vl-edgesplitstmt-lvalues
Gather lvalues from simple, splittable statements.
Vl-edgesplit-atomicstmt-lvalues
Vl-module-edgesplit
Vl-edgesplit-atomicstmt-p
Vl-design-edgesplit