• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Svex-compilation
        • Moddb
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
        • Symbolic-test-vector
        • Vl-to-svex
          • Vl-to-sv
          • Vl-design->sv-design
            • Vl-simpconfig
            • Vl-hierarchy-sv-translation
            • Vl-expr-svex-translation
            • Vl-design->svex-modalist
            • Vl-svstmt
              • Vl-svstmt.lisp
          • Vl-to-sv-main
          • Vl-simplify-sv
          • Vl-user-paramsettings->unparam-names
          • Vl-user-paramsettings->modnames
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl-design->sv-design

Vl-svstmt

Discussion of creating svex assignments from combinational/latch-style always blocks.

Verilog and SystemVerilog don't always cleanly translate to a finite-state-machine semantics, especially when it comes to always blocks that behave as latches. We discuss some of the choices we made in this translation.

Difference between always_comb, always_latch, and plain always

It isn't clear how Verilog simulators distinguish between these constructs. For a simple latch of the form

always_latch if (en) q = d;

Verilog simulators produce identical results if the always_latch is replaced by any of always_comb, always @*, or always @(en or d). However, we treat it differently in the always_comb case, because... (BOZO)

Subtopics

Vl-svstmt.lisp