• 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
          • Vls-commands
          • Vl-descriptionlist-summaries
          • Vls-transdb
          • File-layout
          • Vls-data-p
            • Vls-data
            • Make-vls-data
            • Change-vls-data
            • Honsed-vls-data
            • Make-honsed-vls-data
            • Vls-data->orig-descalist
            • Vls-data->orig
            • Vls-data->good
            • Vls-data->filemap
            • Vls-data->defs
            • Vls-data->bad
          • Ts-queue
          • Vls-showloc
          • Vls-get-plainsrc
          • Vl-description->warnings
          • Vl-describe
          • Vls-port-table
          • Vls-describe
          • Vls-data-from-translation
          • Vl-find-description-insensitive
          • Vls-get-warnings
          • Vls-get-summary
          • Vls-get-origsrc
          • Vls-data-origname-reportcard
          • Vls-get-parents
          • Vls-get-children
          • Vls-get-summaries
          • Vl-ppc-description
          • Vls-get-desctypes
          • Vl-description-summary
          • Start
          • Vl-descalist->descriptions/types
          • Stop
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Server

Vls-data-p

Data that is available to vls-commands.

(vls-data-p x) is a defaggregate of the following fields.

  • good — The successfully translated portion of the design.
        Invariant (vl-design-p good).
  • bad — The portion of the design that had errors or is otherwise unsupported.
        Invariant (vl-design-p bad).
  • orig — The original design, as seen very shortly after parsing.
        Invariant (vl-design-p orig).
  • orig-descalist — A vl-descalist-p binding every description in the original design to its definition.
        Invariant (vl-descalist-okp orig orig-descalist).
  • filemap — Map of all files that were loaded for this translation, for jumping to particular locations.
        Invariant (vl-filemap-p filemap).
  • defs — Summary of all `defines encountered while parsing.
        Invariant (vl-defines-p defs).

Source link: vls-data-p

A vls-data-p structure just aggregates a bunch of data that is produced when we run the translator.

These structures are typically produced by the server as part of its translation-loading scheme.

Subtopics

Vls-data
Raw constructor for vls-data-p structures.
Make-vls-data
Constructor macro for vls-data-p structures.
Change-vls-data
A copying macro that lets you create new vls-data-p structures, based on existing structures.
Honsed-vls-data
Raw constructor for honsed vls-data-p structures.
Make-honsed-vls-data
Constructor macro for honsed vls-data-p structures.
Vls-data->orig-descalist
Access the orig-descalist field of a vls-data-p structure.
Vls-data->orig
Access the orig field of a vls-data-p structure.
Vls-data->good
Access the good field of a vls-data-p structure.
Vls-data->filemap
Access the filemap field of a vls-data-p structure.
Vls-data->defs
Access the defs field of a vls-data-p structure.
Vls-data->bad
Access the bad field of a vls-data-p structure.