• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
        • Esim-vl-find-io
        • Esim-vl-iopattern-p
        • Esim-vl-designwires
        • Esim-vl-wirealist
        • Esim-vl-annotations
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Esim
• Vl2014

Esim-vl

Functions for working with E modules produced by VL.

Subtopics

Esim-vl-find-io

Produce an LSB-first list of E wire names corresponding to a particular input or output of the original Verilog module.

Esim-vl-iopattern-p

Recognize a good :i or :o pattern for a VL-translated module.

Esim-vl-designwires

Produce a flat vl-emodwirelist-p that contains the E names of every bit that is visible in the original Verilog module.

Esim-vl-wirealist

Obtain the vl-wirealist-p for an E module produced by VL.

Esim-vl-annotations

Helper for esim-vl-designwires and esim-vl-wirealist.