• 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
          • Alias-normalization
          • Svex-design-flatten-and-normalize
          • Svex-design-compile
          • Svex-composition
            • Svex-compose-assigns-keys
            • Svex-compose*
            • Svex-compose
            • Svex-compose-svstack
            • Svex-assigns-compose1
            • Svex-assigns-compose
            • Svex-compose-bit-sccs
            • Svex-compose-assigns
            • Svex-replace-var
          • Compile.lisp
          • Assign->segment-drivers
          • Segment-driver-map-resolve
          • Assigns->segment-drivers
        • Moddb
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
        • Symbolic-test-vector
        • Vl-to-svex
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Svex-compilation

Svex-composition

The process of composing together a netlist of svex assignments into full update functions.

Suppose we have a module with a lot of assignment statements. We want to compose together the RHS expressions in order to get the update formula for each wire, in terms of the PIs and registers.

One basic thing to do is DFS through each of the expressions, building full update formulas. Every time we get to a wire, either it is a PI/register or another internal wire. If it is a PI/register, we leave it; if it's an internal wire, either we've seen it before and computed some formula for it, or we descend into its update formula and compute that first.

Two kinds of problems arise when using this strategy. First, there might be variable-level self-loops, e.g.:

wire [5:0] a = b | (a[4:0] << 1);

Here, a looks like a has a self-loop, but in fact each bit only depends on previous bits, so the loop can be unrolled into a combinational formula. This represents a third possibility for when we encounter an internal wire: we've encountered it before, but haven't finished computing a formula for it.

Second, there might be bit-level self-loops. These are bad news but they do sometimes come up, e.g. in latch-based (as opposed to flipflop-based) logic as well as with clock gating where the clock gate signal depends on the output of a register that it gates (depending on how the clock gate is represented in the logic).

To deal with these two problems, we do two further steps after the initial simple DFS composition step; step 2 effectively deals with variable-level self-loops and step 3 deals with bit-level self-loops. The full sequence of steps:

  • 1. Simple depth-first search composition, stopping whenever we reach a variable that is still in the stack.
  • 2. Iterative self-composition of the remaining signals, using caremasks to determine when a variable needs to be composed in. This is implemented in as svex-alist-maskcompose-iter in "mask-compose.lisp".
  • 3. Break up into bits any remaining internal signals that other signals still depend on, then find strongly-connected components of the bit-level dependency graph and try to self-compose those components enough times to resolve further dependencies. Then translate the decomposed signals back into the original namespace.
  • 4. Finally, replace any remaining internal signal dependencies with Xes.

This is implemented svex-assigns-compose.

Subtopics

Svex-compose-assigns-keys
Compose together svex assignments (using svex-compose-dfs) for the listed keys.
Svex-compose*
Compose an svex with a substitution alist. Variables not in the substitution are left in place.
Svex-compose
Compose an svex with a substitution alist. Variables not in the substitution are left in place.
Svex-compose-svstack
Compose an svex with a substitution alist. Variables not in the substitution are left in place.
Svex-assigns-compose1
Given an alist mapping variables to assigned expressions, compose them together into full update functions.
Svex-assigns-compose
Given an alist mapping variables to assigned expressions, compose them together into full update functions.
Svex-compose-bit-sccs
Svex-compose-assigns
Compose together an alist of svex assignments, with no unrolling when variables depend on themselves.
Svex-replace-var
Replace occurrences of a variable within an svex with an svex.