• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Lexer
        • Vl-loadstate
        • Parser
          • Parse-expressions
            • Vl-parse-parameter-value-assignment-hack
            • Vl-erange-p
            • Vl-mixed-binop-list-p
            • Vl-parse-very-simple-type
            • Vl-mark-as-explicit-parens
            • Vl-parse-0+-scope-prefixes
            • Vl-parse-0+-attribute-instances
            • Vl-parse-op
            • Vl-parse-hierarchical-identifier
            • Vl-parse-pva-tail
            • Vl-parse-expression-top
            • Vl-parse-any-sort-of-concatenation
            • Vl-build-indexing-nest
            • Vl-erangetypelist-p
            • Vl-build-range-select-with
            • Vl-build-range-select
            • Vl-parse-simple-type
            • Vl-expr-has-any-atts-p
            • Vl-left-associate-mixed-binop-list
            • Vl-tack-scopes-onto-hid
            • Vl-parse-op-alist-p
            • Vl-make-guts-from-inttoken
            • Vl-parse-range-expression
            • Vl-parse-slice-size
            • Vl-parse-concatenation
            • Vl-parse-stream-expression
            • Vl-parse-1+-stream-expressions-separated-by-commas
            • Vl-parse-stream-concatenation
            • Vl-parse-primary
              • Vl-maybe-parse-base-primary
            • Vl-parse-0+-bracketed-expressions
            • Vl-parse-system-function-call
            • Vl-parse-shift-expression-aux
            • Vl-parse-power-expression-aux
            • Vl-parse-mult-expression-aux
            • Vl-parse-mintypmax-expression
            • Vl-parse-logor-expression-aux
            • Vl-parse-logand-expression-aux
            • Vl-parse-indexed-id-2012
            • Vl-parse-indexed-id-2005
            • Vl-parse-equality-expression-aux
            • Vl-parse-equality-expression
            • Vl-parse-compare-expression-aux
            • Vl-parse-bitxor-expression-aux
            • Vl-parse-bitor-expression-aux
            • Vl-parse-bitand-expression-aux
            • Vl-parse-1+-open-value-ranges
            • Vl-parse-1+-keyval-expression-pairs
            • Vl-parse-unary-expression
            • Vl-parse-shift-expression
            • Vl-parse-qmark-expression
            • Vl-parse-primary-main
            • Vl-parse-primary-cast
            • Vl-parse-power-expression
            • Vl-parse-open-value-range
            • Vl-parse-nonprimary-cast
            • Vl-parse-mult-expression
            • Vl-parse-logor-expression
            • Vl-parse-logand-expression
            • Vl-parse-indexed-id
            • Vl-parse-impl-expression
            • Vl-parse-function-call
            • Vl-parse-expression
            • Vl-parse-compare-expression
            • Vl-parse-bitxor-expression
            • Vl-parse-bitor-expression
            • Vl-parse-bitand-expression
            • Vl-parse-assignment-pattern
            • Vl-parse-add-expression-aux
            • Vl-parse-add-expression
            • Vl-parse-1+-expressions-separated-by-commas
          • Parse-udps
          • Vl-genelements
          • Parse-paramdecls
          • Parse-blockitems
          • Parse-utils
          • Parse-insts
          • Parse-datatype
          • Parse-functions
          • Parse-datatypes
          • Parse-strengths
          • Vl-parse-genvar-declaration
          • Vl-parse
          • Parse-ports
          • Seq
          • Parse-packages
        • Vl-load-merge-descriptions
        • Scope-of-defines
        • Vl-load-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-loadresult
        • Vl-read-file
        • Vl-find-basename/extension
        • Vl-find-file
        • Vl-read-files
        • Extended-characters
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-load-descriptions
        • Vl-load-files
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-parse-primary

Vl-maybe-parse-base-primary

Match basic, atomic kinds of primary expressions, such as primary_literal, this, $, and null, returns a vl-expr-p.

Signature

(vl-maybe-parse-base-primary &key (tokstream 'tokstream) 
                             (config 'config)) 
 
  → 
(mv errmsg? value new-tokstream)

Arguments

config — Guard (vl-loadconfig-p config).

In SystemVerilog-2012, we have:

primary ::= primary_literal
          | 'this'
          | '$'
          | 'null'
          | ... other, more complex things ...

primary_literal ::= number
                  | time_literal
                  | unbased_unsized_literal
                  | string_literal

number ::= integral_number
         | real_number

integral_number ::= decimal_number
                  | octal_number
                  | binary_number
                  | hex_number

This is very similar to the primary production in Verilog-2005:

primary ::= number
          | string
          | ... other, more complex things ...

number ::= decimal_number
         | octal_number
         | binary_number
         | hex_number
         | real_number

We ignore the "other, more complex things" here, and just focus on the simple primaries. Aside from some minor lexical differences at the tips which are handled by the lexer (see for instance lex-strings and lex-numbers) the main difference here is that SystemVerilog adds time literals, unbased unsized literals, this, $, and null.

Definitions and Theorems

Function: vl-maybe-parse-base-primary-fn

(defun vl-maybe-parse-base-primary-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-maybe-parse-base-primary))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when
     (vl-is-token? :vl-inttoken)
     (int := (vl-match))
     (return (make-vl-atom :guts (vl-make-guts-from-inttoken int))))
   (when
    (vl-is-token? :vl-realtoken)
    (real := (vl-match))
    (return
     (b* ((value (vl-echarlist->string (vl-realtoken->etext real))))
       (make-vl-atom :guts (make-vl-real :value value)))))
   (when
     (vl-is-token? :vl-stringtoken)
     (str := (vl-match))
     (return (b* ((value (vl-stringtoken->expansion str)))
               (make-vl-atom :guts (make-vl-string :value value)))))
   (when (eq (vl-loadconfig->edition config)
             :verilog-2005)
         (return nil))
   (when
     (vl-is-token? :vl-extinttoken)
     (ext := (vl-match))
     (return (b* ((value (vl-extinttoken->value ext)))
               (make-vl-atom :guts (make-vl-extint :value value)))))
   (when
    (vl-is-token? :vl-timetoken)
    (time := (vl-match))
    (return
         (b* (((vl-timetoken time) time))
           (make-vl-atom :guts (make-vl-time :quantity time.quantity
                                             :units time.units)))))
   (when
    (vl-is-token? :vl-kwd-null)
    (:= (vl-match))
    (return
       (hons-copy
            (make-vl-atom :guts (make-vl-keyguts :type :vl-null)))))
   (when
    (vl-is-token? :vl-kwd-default)
    (:= (vl-match))
    (return
     (hons-copy
         (make-vl-atom :guts (make-vl-keyguts :type :vl-default)))))
   (when
    (vl-is-token? :vl-kwd-this)
    (:= (vl-match))
    (return
       (hons-copy
            (make-vl-atom :guts (make-vl-keyguts :type :vl-this)))))
   (when
     (vl-is-token? :vl-$)
     (:= (vl-match))
     (return
          (hons-copy
               (make-vl-atom :guts (make-vl-keyguts :type :vl-$)))))
   (return nil))))

Theorem: vl-maybe-parse-base-primary-never-fails

(defthm vl-maybe-parse-base-primary-never-fails
  (not (mv-nth 0 (vl-maybe-parse-base-primary))))

Theorem: vl-maybe-parse-base-primary-result

(defthm vl-maybe-parse-base-primary-result
  (implies
       (and (not (mv-nth 0 (vl-maybe-parse-base-primary)))
            (and t))
       (vl-maybe-expr-p (mv-nth 1 (vl-maybe-parse-base-primary)))))

Theorem: vl-maybe-parse-base-primary-count-strong-on-value

(defthm vl-maybe-parse-base-primary-count-strong-on-value
 (and
   (<= (vl-tokstream-measure
            :tokstream (mv-nth 2 (vl-maybe-parse-base-primary)))
       (vl-tokstream-measure))
   (implies
        (mv-nth 1 (vl-maybe-parse-base-primary))
        (< (vl-tokstream-measure
                :tokstream (mv-nth 2 (vl-maybe-parse-base-primary)))
           (vl-tokstream-measure))))
 :rule-classes ((:rewrite) (:linear)))

Theorem: tokens-nonempty-when-vl-maybe-parse-base-primary

(defthm tokens-nonempty-when-vl-maybe-parse-base-primary
  (b* (((mv ?errmsg val ?new-tokstream)
        (vl-maybe-parse-base-primary)))
    (implies val (consp (vl-tokstream->tokens)))))