• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
        • Name-database
        • Vl-gc
        • Symbol-list-names
        • Ints-from
        • Nats-from
        • Make-lookup-alist
        • Redundant-mergesort
        • Longest-common-prefix
        • Vl-plural-p
        • Vl-remove-keys
        • Vl-merge-contiguous-indices
        • Vl-edition-p
          • Vl-parse-edition
        • Sum-nats
        • Vl-maybe-integer-listp
        • Fast-memberp
        • Nat-listp
        • Max-nats
        • Longest-common-prefix-list
        • Character-list-listp
        • Vl-character-list-list-values-p
        • Remove-from-alist
        • Prefix-of-eachp
        • Vl-string-keys-p
        • Vl-maybe-nat-listp
        • Vl-string-list-values-p
        • String-list-listp
        • Vl-string-values-p
        • True-list-listp
        • Symbol-list-listp
        • Explode-list
        • All-have-len
        • Pos-listp
        • Min-nats
        • Debuggable-and
        • Vl-starname
        • Remove-equal-without-guard
        • Vl-maybe-string-list
        • String-fix
        • Longer-than-p
        • Anyp
        • Fast-alist-free-each-alist-val
        • Not*
        • Free-list-of-fast-alists
        • *nls*
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-edition-p

Vl-parse-edition

Getopt option parser for Verilog editions.

Signature

(vl-parse-edition name explicit-value args) 
  → 
(mv err value rest-args)

Arguments

name — Guard (stringp name).

explicit-value — Guard (or (not explicit-value) (stringp explicit-value)).

args — Guard (string-listp args).

Returns

value — Type (vl-edition-p value).

rest-args — Type (string-listp rest-args), given (force (string-listp args)).

Definitions and Theorems

Function: vl-parse-edition

(defun vl-parse-edition (name explicit-value args)
 (declare (xargs :guard (and (stringp name)
                             (or (not explicit-value)
                                 (stringp explicit-value))
                             (string-listp args))))
 (let ((__function__ 'vl-parse-edition))
  (declare (ignorable __function__))
  (b* (((mv err val args)
        (getopt::parse-string name explicit-value args))
       ((when err)
        (mv err :system-verilog-2012 args))
       ((when (str::istreqv val "Verilog"))
        (mv nil :verilog-2005 args))
       ((when (str::istreqv val "SystemVerilog"))
        (mv nil :system-verilog-2012 args)))
   (mv
    (msg
      "Option ~s0 must be 'Verilog' or 'SystemVerilog', but got ~x1"
      name val)
    :system-verilog-2012 args))))

Theorem: vl-edition-p-of-vl-parse-edition.value

(defthm vl-edition-p-of-vl-parse-edition.value
  (b* (((mv ?err acl2::?value ?rest-args)
        (vl-parse-edition name explicit-value args)))
    (vl-edition-p value))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-parse-edition.rest-args

(defthm string-listp-of-vl-parse-edition.rest-args
  (implies (force (string-listp args))
           (b* (((mv ?err acl2::?value ?rest-args)
                 (vl-parse-edition name explicit-value args)))
             (string-listp rest-args)))
  :rule-classes :rewrite)

Theorem: vl-parse-edition-makes-progress

(defthm vl-parse-edition-makes-progress
  (<= (len (mv-nth 2
                   (vl-parse-edition getopt::name
                                     getopt::explicit-value args)))
      (len args))
  :rule-classes ((:rewrite) (:linear)))