• 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
            • Vl-tnamelist-xdat-files
            • Vl-tnamelist-as-strings
            • Vl-tnamelist-models
            • Vl-tnamelist-bases
            • Vl-tnamelist-p
            • Vls-filter-datestrs
            • Vl-tname
            • Vl-looks-like-legitimate-tname-p
            • Vl-scan-for-tnames-in-base
            • Vl-scan-for-tnames-aux
            • Vl-scan-for-tnames
            • Vl-remove-illegitimate-tnames
            • Vl-find-tname
            • Vl-tnames-for-base
            • Vls-sort-bases
            • Vls-datestr-p
            • Vl-remove-temp-bases
            • Vl-tnames-to-json-aux
            • Vl-tname-xdat-file
            • Vl-tname-as-string
            • Vl-tname-dir
            • Set-vls-root
            • *vls-root*
            • Vl-tnames-to-json
          • Vls-data-p
          • 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

File-layout

Where we look for translation data.

The constant *vls-root* defines the root directory for our translation data.

Each subdirectory of this directory is called a base. At Centaur, we typically run the translator once per day, and we introduce a new base for each day's translations. That is, the base 2010-05-31 contains the translations from May 31, 2010, etc.

Note: as a special convenience, if the name of a base begins with _temp_, we regard it as currently being generated and do not include it in our file scans. Our translation scripts put everything into a directory like _temp_2010-05-31, then finally rename this directory to 2010-05-31 when they're done.

Each base should contain a collection of subdirectories called models. Each model directory contains files like model.sao and esims.sao, which are created by the vl model command. Having multiple models is useful when you are translating many different chips.

Given *vls-root*, the name of a particular base and model are sufficient for identifying where a particular translation exists on the disk.

Subtopics

Vl-tnamelist-xdat-files
(vl-tnamelist-xdat-files x) maps vl-tname-xdat-file across a list.
Vl-tnamelist-as-strings
(vl-tnamelist-as-strings x) maps vl-tname-as-string across a list.
Vl-tnamelist-models
(vl-tnamelist-models x) maps vl-tname->model across a list.
Vl-tnamelist-bases
(vl-tnamelist-bases x) maps vl-tname->base across a list.
Vl-tnamelist-p
(vl-tnamelist-p x) recognizes lists where every element satisfies vl-tname-p.
Vls-filter-datestrs
Filter strings into datestrs and non-datestrs. (See vls-datestr-ps).
Vl-tname
Location of a chip translation
Vl-looks-like-legitimate-tname-p
Return true if the given translation directory (1) includes both model.sao and model.sao.ver files, and (2) the model is compatible with this version of VL.
Vl-scan-for-tnames-in-base
Vl-scan-for-tnames-aux
Vl-scan-for-tnames
Top-level function for scanning for translation names.
Vl-remove-illegitimate-tnames
Vl-find-tname
Vl-tnames-for-base
Vls-sort-bases
Put translations into a nice order.
Vls-datestr-p
Recognize strings of the form YYYY-MM-DD*.
Vl-remove-temp-bases
Vl-tnames-to-json-aux
Vl-tname-xdat-file
Vl-tname-as-string
Vl-tname-dir
Set-vls-root
Smash *vls-root* with something new.
*vls-root*
File system path that says where to look for translations.
Vl-tnames-to-json