• 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
        • Esim-steps
        • Patterns
        • Mod-internal-paths
        • Defmodules
          • Vl-translation-p
            • Vl-translation
            • Make-vl-translation
            • Change-vl-translation
            • Vl-translation-has-module
            • Honsed-vl-translation
            • Make-honsed-vl-translation
            • Vl-translation-get-esim
            • Vl-translation->orig
            • Vl-translation->good
            • Vl-translation->filemap
            • Vl-translation->defines
            • Vl-translation->bad
          • Vl-simplify
          • Defmodules-fn
        • Esim-simplify-update-fns
        • Esim-tutorial
        • Esim-vl
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Defmodules

Vl-translation-p

The result of translating a Verilog or SystemVerilog design.

(vl-translation-p x) is a defaggregate of the following fields.

  • good — Fully translated modules, etc., for whatever subset of the overall design we were able to successfully translate. This is the "good subset" of the design.
        Invariant (vl-design-p good).
  • bad — Partially translated modules, etc., that, for whatever reason, we were unable to successfully translate. The modules here will typically have fatal warnings. This This is the "bad subset" or at least the "unsupported subset" of the design.
        Invariant (vl-design-p bad).
  • orig — The raw, unsimplified design that we obtained immediately after parsing. This can be useful for pretty-printing and understanding modules.
        Invariant (vl-design-p orig).
  • filemap — The actual Verilog source code that was read. Occasionally this is useful for understanding warnings that refer to particular file locations.
        Invariant (vl-filemap-p filemap).
  • defines — Records all of the `define directives that were encountered during parsing, and their final values. This is sometimes useful for extracting definitions like opcodes, etc.
        Invariant (vl-defines-p defines).

Source link: vl-translation-p

Translation objects are most commonly produced by the defmodules command.

Subtopics

Vl-translation
Raw constructor for vl-translation-p structures.
Make-vl-translation
Constructor macro for vl-translation-p structures.
Change-vl-translation
A copying macro that lets you create new vl-translation-p structures, based on existing structures.
Vl-translation-has-module
Check whether a module was successfully translated.
Honsed-vl-translation
Raw constructor for honsed vl-translation-p structures.
Make-honsed-vl-translation
Constructor macro for honsed vl-translation-p structures.
Vl-translation-get-esim
Get an E Module for a successfully translated module.
Vl-translation->orig
Access the orig field of a vl-translation-p structure.
Vl-translation->good
Access the good field of a vl-translation-p structure.
Vl-translation->filemap
Access the filemap field of a vl-translation-p structure.
Vl-translation->defines
Access the defines field of a vl-translation-p structure.
Vl-translation->bad
Access the bad field of a vl-translation-p structure.