• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-fixpoint-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Moddb
        • Svex-compilation
          • Alias-normalization
          • Svex-design-flatten-and-normalize
          • Svex-design-compile
          • Svex-composition
          • Compile.lisp
          • Assign->netassigns
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
        • Symbolic-test-vector
        • Vl-to-svex
      • Vwsim
      • Fgl
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Sv

Svex-compilation

Turning a hierarchical SVEX design into a finite state machine.

The function svex-design-compile extracts a finite state machine representation from a hierarchical SVEX design. See also defsvtv, defsvtv$, and defcycle, which all perform this process and subsequently perform some amount of unrolling of the resulting finite state machine in order to produce either a pipeline representation (defsvtv and defsvtv$) or a cycle FSM (defcycle).

We follow these steps to turn an svex module hierarchy into a finite-state machine representation:

  • Enumerate wires. We walk over each module and count the wires contained in it and all its submodules. We store this information in a module database (see moddb), which allows us to both look up a hierarchical names and get their wire indices or vice versa.
  • Translate the module hierarchy's assignments and aliases by replacing wire names with indices (see modalist-named->indexed).
  • Flatten the assignments, aliases, and stateholding elements (see svex-mod->flatten).
  • Use the flattened aliases to compute a canonical alias table, mapping every wire to a canonical representation (see canonicalize-alias-pairs).
  • Canonicalize the wires in the flattened assignment list and stateholding elements using the alias table (see assigns-subst).
  • Convert the lists of assignments and stateholding elements, which may have arbitrary LHS expressions as the left-hand sides, into a list of assignments to variables. This involves segmenting each assignment into separate assignments to its individual LHS components (see assigns->netassigns), and then for wires that have multiple assignments, resolving these together to obtain a single RHS (see netassigns->resolves).
  • Compose assignments together to obtain the full 0-delay formulas for each canonical wire and full update functions for each state bit; that is, formulas in terms of primary inputs and previous states (see svex-assigns-compose).

Subtopics

Alias-normalization
The process of computing a canonical form for each wire in the module hierarchy.
Svex-design-flatten-and-normalize
Flatten a hierarchical SV design and apply alias normalization to it.
Svex-design-compile
Compile a hierarchical SVEX design into a finite state machine.
Svex-composition
The process of composing together a netlist of svex assignments into full update functions.
Compile.lisp
Assign->netassigns
Turns an assignment (possibly to parts of wires) into several assignments to whole wires.