• 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
            • Vl-modulelist-check-port-bits
            • Vl-module-check-port-bits
        • 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
  • E-conversion

Port-bit-checking

A well-formedness check to ensure that ports and port declarations agree, and are simple enough for E conversion.

Before generating E modules, we do a global pass over the module list and make sure that we can generate the port pattern for each module appropriately.

Subtopics

Vl-modulelist-check-port-bits
(vl-modulelist-check-port-bits x) maps vl-module-check-port-bits across a list.
Vl-module-check-port-bits
Ensure the port pattern for a module is reasonable.