• Top
    • Documentation
    • Books
    • 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-res-sigma-p
            • Vl-res-rewrite-occs
            • Vl-add-res-modules
            • Vl-make-res-occs
          • 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
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • E-conversion

Resolving-multiple-drivers

How we replace multiply driven wires with explicit resolution modules.

We want every wire in our E modules to have at most one driver, but the list of occurrences we get from vl-modinstlist-to-eoccs could easily have multiple occurrences all driving the same wire. We now introduce a transform to simplify a list of E occurrences, eliminating multiply driven wires by inserting explicit resolution modules.

Note: In this transform we assume that the module's primary inputs are not driven by any occurrence. This is something we explicitly check for in vl-module-make-esim; see the warning about :vl-backflow there.

Given this assumption, we basically need to do three things:

  1. Identify when a wire W has multiple occurrences driving it. Fortunately, this is completely trivial:
    (duplicated-members (collect-signal-list :o occs))
  2. Rewrite each occurrence driving W so that it instead drives some new, unique, freshly generated wire (say W_1, W_2, ...). We also need to remember the names we used for each wire, for step 3. We do this with the function vl-res-rewrite-occs.
  3. Insert new occurrences that drive W with the (RES W_1 W_2 ...). This is done with vl-make-res-occs.

The top-level function is vl-add-res-modules, and it just stitches these steps together.

Subtopics

Vl-res-sigma-p
An alist that records the fresh wires we introduce for multiply driven wires.
Vl-res-rewrite-occs
Rewrite occurrences to drive new, fresh wires instead of multiply driven wires.
Vl-add-res-modules
Top-level function for resolving multiple drivers in a list of E occurrences.
Vl-make-res-occs
Convert the vl-res-sigma-p database into a list of E occurrences to drive each multiply driven wire.