• 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
              • Vl-edgesynth-stmt-p
              • Vl-edgetable-p
              • Vl-always-edgesynth
              • Vl-edgesynth-merge-data-ifs
              • Vl-assignstmtlist->controls
              • Vl-assignstmtlist->lhses
              • Vl-assignstmtlist->rhses
              • Vl-edgesynth-flatten-data-ifs
              • Vl-edgesynth-pattern-match
              • Nedgeflop
                • Vl-make-same-bitselect-from-each
                • Vl-primitive-mkports
                • Vl-nedgeflop-ifstmt
                • Vl-make-1-bit-n-edge-flop
                • Vl-make-nedgeflop-insts
                • Vl-nedgeflop-always
                • Vl-nedgeflop-clkedge-assigns
                • Vl-nedgeflop-update-sexpr
                • Vl-nedgeflop-e-wires
                • Vl-make-delay-assigns
                • Vl-nedgeflop-posedge-clks
                • Vl-nedgeflop-data-mux
                • Vl-nedgeflop-some-edge-sexpr
                • Vl-modinsts-add-atts
                • Vl-nedgeflop-or-edges
              • Vl-edgesynth-make-data-inputs
              • Vl-edgesynth-make-clock-inputs
              • Vl-edgesynth-stmt-clklift
              • Vl-edgesynth-blockelim
              • Vl-alwayslist-edgesynth
              • Vl-edgesynth-create
              • Vl-edgesynth-classify-iftest
              • Vl-module-edgesynth
              • Vl-edgesynth-normalize-ifs
              • Vl-edgesynth-delays-okp
              • Vl-edgesynth-stmt-assigns
              • Vl-make-edgetable
              • Vl-edgesynth-sort-edges
              • Vl-modulelist-edgesynth
              • Vl-modulelist-edgesynth-aux
              • Vl-assignstmtlist-p
              • Vl-edgesynth-edgelist-p
              • Vl-assigncontrols-p
              • Vl-edgesynth-stmt-conditions
              • Vl-edgesynth-edge-p
              • Vl-design-edgesynth
              • Vl-edgesynth-get-delay
              • Vl-edgesynth-iftype-p
              • Edge-tables
            • Stmtrewrite
            • 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
  • Edgesynth
  • Primitives

Nedgeflop

Generation of new primitives for edge-triggered always blocks.

See edgesynth for an overview of how we handle edge-triggered always blocks.

To support these blocks, VL creates primitive flip-flop modules with some number of edges. For instance, the primitive 3-edge flop can be described as follows in Verilog, and could be used to implement a flip-flop with, e.g., asynchronous set and reset signals.

module VL_1_BIT_3_EDGE_FLOP (q, d0, d1, d2, clk0, clk1, clk2);
  output reg q;
  input d0, d1, d2;
  input clk0, clk1, clk2;
  always @(posedge clk0 or posedge clk1)
    if (clk0)
       q <= d0
    else if (clk1)
       q <= d1;
    else
       q <= d2;
endmodule

The functions below generate these primitive modules and their corresponding esim implementations.

Subtopics

Vl-make-same-bitselect-from-each
(vl-make-same-bitselect-from-each x index) maps vl-make-bitselect across a list.
Vl-primitive-mkports
Helper function for creating lists of primitive port declarations.
Vl-nedgeflop-ifstmt
Build the Verilog if-statement for a primitive n-edge flop.
Vl-make-1-bit-n-edge-flop
Build the primitive VL module for an n-edge flop.
Vl-make-nedgeflop-insts
Vl-nedgeflop-always
Build the Verilog always statement for a primitive n-edge flop.
Vl-nedgeflop-clkedge-assigns
Vl-nedgeflop-update-sexpr
Build a 4v-sexpr with the update function upon a posedge.
Vl-nedgeflop-e-wires
Vl-make-delay-assigns
Vl-nedgeflop-posedge-clks
Build the Verilog sensitivity list for a primitive n-edge flop.
Vl-nedgeflop-data-mux
Vl-nedgeflop-some-edge-sexpr
Build a 4v-sexpr that captures when any clock has just had a posedge.
Vl-modinsts-add-atts
Vl-nedgeflop-or-edges