• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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

• File-layout

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.

Signature

(vl-looks-like-legitimate-tname-p x state) → (mv legitp state)

Arguments

x — Guard (vl-tname-p x).

Returns

legitp — Type (booleanp legitp).

state — Type (state-p1 state), given (force (state-p1 state)).

Definitions and Theorems

Function: vl-looks-like-legitimate-tname-p

(defun vl-looks-like-legitimate-tname-p (x state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (vl-tname-p x)))
  (let ((__function__ 'vl-looks-like-legitimate-tname-p))
    (declare (ignorable __function__))
    (b* ((tdir (vl-tname-dir x))
         ((mv err files state)
          (oslib::ls-files tdir))
         ((when err)
          (cw "; NOTE: Error listing ~x0: ~@1~%"
              tdir err)
          (mv nil state))
         ((unless (and (member-equal "model.sao" files)
                       (member-equal "model.sao.ver" files)))
          (mv nil state))
         (verfile (oslib::catpath tdir "model.sao.ver"))
         ((mv ver state)
          (acl2::read-file-as-string verfile state))
         ((unless ver) (mv nil state))
         (found (str::trim ver))
         (expect (str::trim *vl-current-syntax-version*))
         ((unless (equal found expect))
          (mv nil state)))
      (mv t state))))

Theorem: booleanp-of-vl-looks-like-legitimate-tname-p.legitp

(defthm booleanp-of-vl-looks-like-legitimate-tname-p.legitp
  (b* (((mv ?legitp acl2::?state)
        (vl-looks-like-legitimate-tname-p x state)))
    (booleanp legitp))
  :rule-classes :type-prescription)

Theorem: state-p1-of-vl-looks-like-legitimate-tname-p.state

(defthm state-p1-of-vl-looks-like-legitimate-tname-p.state
  (implies (force (state-p1 state))
           (b* (((mv ?legitp acl2::?state)
                 (vl-looks-like-legitimate-tname-p x state)))
             (state-p1 state)))
  :rule-classes :rewrite)