• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
        • Symbolic-test-vectors
        • Esim-primitives
        • E-conversion
          • Vl-ealist-p
          • Modinsts-to-eoccs
          • Vl-module-make-esim
          • Exploding-vectors
          • Resolving-multiple-drivers
          • Vl-modulelist-make-esims
          • Vl-module-check-e-ok
          • Vl-collect-design-wires
          • Adding-z-drivers
          • Vl-design-to-e
          • Vl-design-to-e-check-ports
          • Vl-design-to-e-main
          • Port-bit-checking
        • Esim-steps
        • Patterns
        • Mod-internal-paths
        • Defmodules
        • Esim-simplify-update-fns
        • Esim-tutorial
        • Esim-vl
      • Vl2014
      • Sv
      • Vwsim
      • Fgl
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Esim

E-conversion

Translation from simplified Verilog modules into E modules.

The conversion from Verilog to E is mostly straightforward because here we only try to support an extremely limited subset of Verilog. The basic idea is that other transforms should first be used to simplify more complex, "original" input modules into this simple subset.

Here are some basic expectations:

  • Each module we need to process will include net declarations and submodule instances, but will not have any assignments, gates, always blocks, parameters, registers, variables, etc. These other constructs should be simplified away before E conversion.
  • Each module instance will have well-formed port connections that contain only sliceable expressions. This lets us deal with everything purely at the bit level.

We have checks to ensure our assumptions hold, and these checks will result in fatal warnings if the modules contain unsupported constructs. See in particular vl-module-check-e-ok and vl-module-check-port-bits.

We process the modules in dependency order, and aside from sanity checking there are basically two steps for each module we need to convert:

  1. We produce a preliminary E module by exploding the module's vectors into individual bits, and converting the module instances into E occurrences for the submodules.
  2. This preliminary E module is almost a proper E module, but it might have some wires that are driven by multiple occurrences. As a second step, we rewrite the preliminary module to resolve these multiply driven wires. This ensures that every wire has exactly one driver.

Some final sanity checking is done to ensure that the module's inputs and outputs are properly marked and there is no "backflow" occurring.

The resulting E module for each Verilog module is saved in the esim field of each vl-module-p.

Subtopics

Vl-ealist-p
Alist binding module names to E modules.
Modinsts-to-eoccs
How we convert Verilog modules instances into (preliminary) E module occurrences.
Vl-module-make-esim
Convert a Verilog module into an E module.
Exploding-vectors
How we convert Verilog wires (which might be vectors) into E wires (which are just bits).
Resolving-multiple-drivers
How we replace multiply driven wires with explicit resolution modules.
Vl-modulelist-make-esims
Extend vl-module-make-esim across a list of modules.
Vl-module-check-e-ok
Check for unsupported constructs.
Vl-collect-design-wires
Collect all symbols for design-visible wires and return them as a flat list of bits.
Adding-z-drivers
How we ensure every wire is driven.
Vl-design-to-e
Top-level function for E conversion.
Vl-design-to-e-check-ports
Make sure that the module port/port-declarations agree and that there are no unsupported constructs.
Vl-design-to-e-main
Port-bit-checking
A well-formedness check to ensure that ports and port declarations agree, and are simple enough for E conversion.