• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
          • Preprocessor
          • Vl-loadconfig
          • Vl-loadstate
          • Lexer
          • Parser
            • Parse-expressions
              • Vl-expressions->paramvalues
              • Vl-erange-p
              • Vl-mixed-binop-list-p
              • Vl-parse-very-simple-type
              • Vl-parse-0+-scope-prefixes
              • Vl-parse-0+-attribute-instances
              • Vl-parse-hierarchical-identifier
              • Vl-parse-op
              • Vl-mark-as-explicit-parens
              • Vl-parse-expression-top
              • Vl-parse-any-sort-of-concatenation-aux
              • Vl-parse-datatype-or-implicit
              • Vl-vardeclassignlist-p
              • Vl-build-range-select
              • Vl-parse-scopename
              • Vl-parse-optional-edge-identifier
              • Vl-make-structmembers
              • Vl-erangetypelist-p
              • Vl-coretypekwd->info
              • Vl-streamexpr-with
              • Vl-parse-simple-type
              • Vl-expr-has-any-atts-p
              • Vl-vardeclassignlist-newfree-p
              • Vl-tack-scopes-onto-hid
              • Vl-left-associate-mixed-binop-list
              • Vl-extend-atts-with-linestart
              • Vl-parse-op-alist-p
              • Vl-make-guts-from-inttoken
              • Vl-extend-expr-with-linestart
              • Vl-interpret-expr-as-type
              • Vl-initial-patternkey-from-expr
              • Vl-parse-range-expression
              • Vl-parse-slice-size
              • Vl-parse-concatenation
              • Vl-parse-stream-expression
              • Vl-plausible-start-of-range-p
              • Vl-parse-any-sort-of-concatenation
              • Vl-parse-1+-stream-expressions-separated-by-commas
              • Vl-parse-stream-concatenation
              • Vl-parse-primary
              • Vl-parse-datatype
              • Vl-parse-0+-bracketed-expressions
              • Vl-parse-variable-decl-assignment
              • Vl-parse-system-function-call
              • Vl-parse-shift-expression-aux
              • Vl-parse-power-expression-aux
              • Vl-parse-parameter-value-assignment
              • Vl-parse-named-parameter-assignment
              • Vl-parse-mult-expression-aux
              • Vl-parse-mintypmax-expression
              • Vl-parse-logor-expression-aux
              • Vl-parse-logand-expression-aux
              • Vl-parse-list-of-parameter-assignments
              • Vl-parse-indexed-id-2012
              • Vl-parse-indexed-id-2005
              • Vl-parse-expression-without-failure
              • Vl-parse-expr-or-clocking-event
              • Vl-parse-event-expression-2012
              • Vl-parse-event-expression-2005
              • Vl-parse-event-expression
              • Vl-parse-equality-expression-aux
              • Vl-parse-equality-expression
              • Vl-parse-enum-name-declaration
              • Vl-parse-compare-expression-aux
              • Vl-parse-bitxor-expression-aux
              • Vl-parse-bitor-expression-aux
              • Vl-parse-bitand-expression-aux
              • Vl-parse-associative-dimension
              • Vl-parse-1+-variable-decl-assignments-separated-by-commas
              • Vl-parse-1+-open-value-ranges
              • Vl-parse-1+-keyval-expression-pairs
              • Vl-parse-1+-enum-name-declarations-separated-by-commas
              • Vl-parse-0+-variable-dimensions
              • Vl-parse-0+-unpacked-dimensions
              • Vl-parse-0+-packed-dimensions
              • Vl-parse-variable-dimension
              • Vl-parse-unpacked-dimension
              • Vl-parse-unary-expression
              • Vl-parse-sysfuncall-args
              • Vl-parse-structmembers
              • Vl-parse-structmember
              • Vl-parse-shift-expression
              • Vl-parse-scoped-hid
              • Vl-parse-rhs
              • Vl-parse-range
              • Vl-parse-queue-dimension
              • Vl-parse-qmark-expression
              • Vl-parse-pva-tail
              • Vl-parse-primary-main
              • Vl-parse-primary-cast
              • Vl-parse-power-expression
              • Vl-parse-patternkey
              • Vl-parse-param-expression
              • Vl-parse-packeddimension
              • Vl-parse-open-value-range
              • Vl-parse-nonprimary-cast
              • Vl-parse-mult-expression
              • Vl-parse-logor-expression
              • Vl-parse-logand-expression
              • Vl-parse-list-of-ordered-parameter-assignments
              • Vl-parse-list-of-named-parameter-assignments
              • Vl-parse-indexed-id
              • Vl-parse-impl-expression
              • Vl-parse-function-call
              • Vl-parse-expression
              • Vl-parse-enum-base-type
              • Vl-parse-datatype-or-void
              • Vl-parse-core-data-type
              • Vl-parse-compare-expression
              • Vl-parse-clocking-event
              • Vl-parse-call-plainargs-aux
              • Vl-parse-call-plainargs
              • Vl-parse-call-namedargs-aux
              • Vl-parse-call-namedargs
              • Vl-parse-call-namedarg-pair
              • 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
              • Vl-parse-0+-ranges
            • Parse-udps
            • Parse-statements
            • Parse-property
            • Vl-genelements
            • Parse-paramdecls
            • Parse-blockitems
            • Parse-utils
            • Parse-insts
            • Parse-functions
            • Parse-assignments
            • Parse-clocking
            • Parse-strengths
            • Vl-parse-genvar-declaration
            • Vl-parse
            • Parse-netdecls
            • Parse-asserts
            • Vl-maybe-parse-lifetime
            • Parse-dpi-import-export
            • Parse-ports
            • Parse-timeunits
            • Seq
            • Parse-packages
            • Parse-eventctrl
          • Vl-load-merge-descriptions
          • Vl-find-basename/extension
          • Vl-load-file
          • Vl-loadresult
          • Scope-of-defines
          • Vl-find-file
          • Vl-flush-out-descriptions
          • Vl-description
          • Vl-read-file
          • Vl-includeskips-report-gather
          • Vl-load-main
          • Extended-characters
          • Vl-load
          • Vl-load-description
          • Vl-descriptions-left-to-load
          • Inject-warnings
          • Vl-preprocess-debug
          • Vl-write-preprocessor-debug-file
          • Vl-read-file-report-gather
          • Vl-load-descriptions
          • Vl-load-files
          • Translate-off
          • Vl-load-read-file-hook
          • Vl-read-file-report
          • Vl-loadstate-pad
          • Vl-load-summary
          • Vl-collect-modules-from-descriptions
          • Vl-loadstate->warnings
          • Vl-iskips-report
          • Vl-descriptionlist
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Parser

Parse-expressions

Parser for Verilog and SystemVerilog expressions.

This is very complicated because everything about expressions is mutually recursive. Most of the functions here correspond to particular productions in the grammars of the Verilog-2005 or SystemVerilog-2012. A few high-level notes:

  • The documentation for each function generally describes the grammar productions that are being implemented.
  • We generally simplify the grammar rules by removing any bare "aliases" such as base_expression ::= expression and attr_name ::= identifier.
  • We do not try to implement any separation between "ordinary" expressions and "constant" expressions. I think the whole treatment of constant expressions as a syntactic construct is somewhat misguided. It is difficult to imagine truly handling constant expressions at parse time. For instance, in a parameterized module with, say, a width parameter, you really want to resolve expressions like width-1 into constants and treat them as constant indexes. But you can't do this until you know the values for these parameters, which you don't know until you've read all the instances of the module, etc.

Definitions and Theorems

Function: vl-parse-packeddimension-fn

(defun vl-parse-packeddimension-fn (tokstream config)
 (declare (xargs :measure-debug t))
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-packeddimension))
  (declare (ignorable __function__))
  (seq
    tokstream
    (:= (vl-match-token :vl-lbrack))
    (when (vl-is-token? :vl-rbrack)
          (:= (vl-match))
          (return :vl-unsized-dimension))
    (msb :s= (vl-parse-expression))
    (:= (vl-match-token :vl-colon))
    (lsb := (vl-parse-expression))
    (:= (vl-match-token :vl-rbrack))
    (return
         (vl-range->dimension (make-vl-range :msb msb :lsb lsb))))))

Function: vl-parse-0+-packed-dimensions-fn

(defun vl-parse-0+-packed-dimensions-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-0+-packed-dimensions))
    (declare (ignorable __function__))
    (seq tokstream
         (unless (vl-is-token? :vl-lbrack)
                 (return nil))
         (first :s= (vl-parse-packeddimension))
         (rest := (vl-parse-0+-packed-dimensions))
         (return (cons first rest)))))

Function: vl-parse-unpacked-dimension-fn

(defun vl-parse-unpacked-dimension-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-unpacked-dimension))
  (declare (ignorable __function__))
  (seq
    tokstream
    (:= (vl-match-token :vl-lbrack))
    (msb :s= (vl-parse-expression))
    (when (vl-is-token? :vl-colon)
          (:= (vl-match))
          (lsb := (vl-parse-expression)))
    (:= (vl-match-token :vl-rbrack))
    (return
         (if lsb (make-vl-range :msb msb :lsb lsb)
           (make-vl-range
                :msb (vl-make-index 0)
                :lsb (make-vl-binary :op :vl-binary-minus
                                     :left msb
                                     :right (vl-make-index 1))))))))

Function: vl-parse-0+-unpacked-dimensions-fn

(defun vl-parse-0+-unpacked-dimensions-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-0+-unpacked-dimensions))
    (declare (ignorable __function__))
    (seq tokstream
         (unless (vl-is-token? :vl-lbrack)
                 (return nil))
         (first :s= (vl-parse-unpacked-dimension))
         (rest := (vl-parse-0+-unpacked-dimensions))
         (return (cons first rest)))))

Function: vl-parse-queue-dimension-fn

(defun vl-parse-queue-dimension-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-queue-dimension))
    (declare (ignorable __function__))
    (seq tokstream
         (:= (vl-match-token :vl-lbrack))
         (:= (vl-match-token :vl-$))
         (when (vl-is-token? :vl-colon)
               (:= (vl-match))
               (maxsize := (vl-parse-expression)))
         (:= (vl-match-token :vl-rbrack))
         (return (make-vl-dimension-queue :maxsize maxsize)))))

Function: vl-parse-core-data-type-fn

(defun vl-parse-core-data-type-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (declare
    (xargs :guard (vl-is-some-token? *vl-core-data-type-keywords*)))
 (let ((__function__ 'vl-parse-core-data-type))
  (declare (ignorable __function__))
  (b* ((entry (vl-coretypekwd->info
                   (vl-token->type (car (vl-tokstream->tokens)))))
       ((vl-coredatatype-info entry) entry))
   (seq
    tokstream (:= (vl-match-any))
    (when
        (and entry.takes-signingp
             (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned)))
        (signing := (vl-match)))
    (when entry.takes-dimensionsp
          (dims := (vl-parse-0+-packed-dimensions)))
    (return
        (let ((ans (make-vl-coretype
                        :name entry.coretypename :signedp
                        (if signing (if (eq (vl-token->type signing)
                                            :vl-kwd-signed)
                                        t
                                      nil)
                          entry.default-signedp)
                        :pdims dims)))
          (mbe :logic ans :exec
               (if (atom dims)
                   (hons-copy ans)
                 ans))))))))

Function: vl-parse-enum-base-type-fn

(defun vl-parse-enum-base-type-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-enum-base-type))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when
    (vl-is-token? :vl-idtoken)
    (name := (vl-match))
    (when (vl-is-token? :vl-lbrack)
          (dim := (vl-parse-packeddimension)))
    (return
     (make-vl-usertype
      :name
      (make-vl-scopeexpr-end
           :hid (make-vl-hidexpr-end :name (vl-idtoken->name name)))
      :pdims (and dim (list dim)))))
   (when
    (vl-is-some-token? '(:vl-kwd-bit :vl-kwd-logic :vl-kwd-reg))
    (type := (vl-match))
    (when (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned))
          (signing := (vl-match)))
    (when (vl-is-token? :vl-lbrack)
          (dim := (vl-parse-packeddimension)))
    (return
        (make-vl-coretype :name (case (vl-token->type type)
                                      (:vl-kwd-bit :vl-bit)
                                      (:vl-kwd-logic :vl-logic)
                                      (:vl-kwd-reg :vl-reg))
                          :signedp (and signing
                                        (eq (vl-token->type signing)
                                            :vl-kwd-signed))
                          :pdims (and dim (list dim)))))
   (type := (vl-match-some-token
                 '(:vl-kwd-byte :vl-kwd-shortint
                                :vl-kwd-int :vl-kwd-longint
                                :vl-kwd-integer :vl-kwd-time)))
   (when (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned))
         (signing := (vl-match)))
   (return
        (make-vl-coretype
             :name (case (vl-token->type type)
                         (:vl-kwd-byte :vl-byte)
                         (:vl-kwd-shortint :vl-shortint)
                         (:vl-kwd-int :vl-int)
                         (:vl-kwd-longint :vl-longint)
                         (:vl-kwd-integer :vl-integer)
                         (:vl-kwd-time :vl-time))
             :signedp (cond (signing (eq (vl-token->type signing)
                                         :vl-kwd-signed))
                            ((eq (vl-token->type type) :vl-kwd-time)
                             nil)
                            (t t)))))))

Function: vl-parse-enum-name-declaration-fn

(defun vl-parse-enum-name-declaration-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-enum-name-declaration))
  (declare (ignorable __function__))
  (seq
   tokstream
   (name := (vl-match-token :vl-idtoken))
   (when
    (vl-is-token? :vl-lbrack)
    (:= (vl-match))
    (left := (vl-match-token :vl-inttoken))
    (when
       (or (not (vl-inttoken->value left))
           (member #\'
                   (vl-echarlist->chars (vl-inttoken->etext left))))
       (return-raw (vl-parse-error "Illegal enum index")))
    (when
     (vl-is-token? :vl-colon)
     (:= (vl-match))
     (right := (vl-match-token :vl-inttoken))
     (when
      (or (not (vl-inttoken->value right))
          (member #\'
                  (vl-echarlist->chars (vl-inttoken->etext right))))
      (return-raw (vl-parse-error "Illegal enum index"))))
    (:= (vl-match-token :vl-rbrack)))
   (when (vl-is-token? :vl-equalsign)
         (:= (vl-match))
         (value := (vl-parse-expression)))
   (when
       (and left (not right)
            (equal (vl-inttoken->value left) 0))
       (return-raw (vl-parse-error "Illegal enum item index [0].")))
   (return
    (make-vl-enumitem
     :name (vl-idtoken->name name)
     :range
     (cond
        ((not left) nil)
        ((not right)
         (make-vl-range
              :msb (vl-make-index 0)
              :lsb (vl-make-index (- (vl-inttoken->value left) 1))))
        (t (make-vl-range
                :msb (vl-make-index (vl-inttoken->value left))
                :lsb (vl-make-index (vl-inttoken->value right)))))
     :value value)))))

Function: vl-parse-1+-enum-name-declarations-separated-by-commas-fn

(defun vl-parse-1+-enum-name-declarations-separated-by-commas-fn
       (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let
    ((__function__
          'vl-parse-1+-enum-name-declarations-separated-by-commas))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-enum-name-declaration))
   (when
    (vl-is-token? :vl-comma)
    (:= (vl-match))
    (rest
       := (vl-parse-1+-enum-name-declarations-separated-by-commas)))
   (return (cons first rest)))))

Function: vl-parse-rhs-fn

(defun vl-parse-rhs-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-rhs))
  (declare (ignorable __function__))
  (seq
   tokstream
   (unless (vl-is-token? :vl-kwd-new)
           (expr := (vl-parse-expression))
           (return (make-vl-rhsexpr :guts expr)))
   (:= (vl-match))
   (when (vl-is-token? :vl-lbrack)
         (:= (vl-match))
         (arrsize :s= (vl-parse-expression))
         (:= (vl-match-token :vl-rbrack))
         (when (vl-is-token? :vl-lparen)
               (:= (vl-match))
               (arg1 := (vl-parse-expression))
               (:= (vl-match-token :vl-rparen))
               (return (make-vl-rhsnew :arrsize arrsize
                                       :args (list arg1))))
         (return (make-vl-rhsnew :arrsize arrsize)))
   (return-raw
     (b*
      ((backup (vl-tokstream-save))
       ((mv err1 args tokstream)
        (seq tokstream
             (:= (vl-match-token :vl-lparen))
             (args := (vl-parse-1+-expressions-separated-by-commas))
             (:= (vl-match-token :vl-rparen))
             (return args)))
       ((unless err1)
        (mv nil
            (make-vl-rhsnew :arrsize nil :args args)
            tokstream))
       (tokstream (vl-tokstream-restore backup))
       ((mv err2 arg1 tokstream)
        (vl-parse-expression))
       ((unless err2)
        (mv nil
            (make-vl-rhsnew :arrsize nil
                            :args (list arg1))
            tokstream))
       (tokstream (vl-tokstream-restore backup)))
      (mv nil
          (make-vl-rhsnew :arrsize nil :args nil)
          tokstream))))))

Function: vl-parse-range-fn

(defun vl-parse-range-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-range))
    (declare (ignorable __function__))
    (seq tokstream
         (:= (vl-match-token :vl-lbrack))
         (msb :s= (vl-parse-expression))
         (:= (vl-match-token :vl-colon))
         (lsb := (vl-parse-expression))
         (:= (vl-match-token :vl-rbrack))
         (return (make-vl-range :msb msb :lsb lsb)))))

Function: vl-parse-0+-ranges-fn

(defun vl-parse-0+-ranges-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-0+-ranges))
    (declare (ignorable __function__))
    (seq tokstream
         (unless (vl-plausible-start-of-range-p)
                 (return nil))
         (first :s= (vl-parse-range))
         (rest := (vl-parse-0+-ranges))
         (return (cons first rest)))))

Function: vl-parse-datatype-or-void-fn

(defun vl-parse-datatype-or-void-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-datatype-or-void))
    (declare (ignorable __function__))
    (seq tokstream
         (when (vl-is-token? :vl-kwd-void)
               (:= (vl-match-any))
               (return (make-vl-coretype :name :vl-void)))
         (type :s= (vl-parse-datatype))
         (return type))))

Function: vl-parse-datatype-fn

(defun vl-parse-datatype-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-datatype))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when
    (vl-is-token? :vl-kwd-type)
    (return-raw
       (vl-parse-error "type references are not yet implemented.")))
   (when
    (vl-is-token? :vl-kwd-virtual)
    (when
        t
        (return-raw
             (vl-parse-error
                  "Virtual interface datatypes are not supported")))
    (:= (vl-match))
    (id := (vl-match-token :vl-idtoken))
    (when (vl-is-token? :vl-pound)
          (params := (vl-parse-parameter-value-assignment)))
    (return
     (make-vl-usertype
        :name
        (make-vl-scopeexpr-end
             :hid (make-vl-hidexpr-end :name (vl-idtoken->name id)))
        :virtual-intfc t
        :intfc-params params)))
   (when (vl-is-some-token? *vl-core-data-type-keywords*)
         (ret := (vl-parse-core-data-type))
         (return ret))
   (when
    (vl-is-some-token? '(:vl-kwd-struct :vl-kwd-union))
    (kind := (vl-match))
    (when (and (vl-is-token? :vl-kwd-tagged)
               (eq (vl-token->type kind)
                   :vl-kwd-union))
          (tagged := (vl-match)))
    (when
        (vl-is-token? :vl-kwd-packed)
        (packed := (vl-match))
        (when (vl-is-some-token? '(:vl-kwd-signed :vl-kwd-unsigned))
              (signed := (vl-match))))
    (:= (vl-match-token :vl-lcurly))
    (members :s= (vl-parse-structmembers))
    (:= (vl-match-token :vl-rcurly))
    (dims := (vl-parse-0+-packed-dimensions))
    (return (b* ((packedp (acl2::bool-fix packed))
                 (signedp (and signed
                               (eq (vl-token->type signed)
                                   :vl-kwd-signed)))
                 ((when (eq (vl-token->type kind)
                            :vl-kwd-struct))
                  (make-vl-struct :packedp packedp
                                  :signedp signedp
                                  :members members
                                  :pdims dims)))
              (make-vl-union :packedp packedp
                             :signedp signedp
                             :taggedp (acl2::bool-fix tagged)
                             :members members
                             :pdims dims))))
   (when
    (vl-is-token? :vl-kwd-enum)
    (:= (vl-match))
    (unless (vl-is-token? :vl-lcurly)
            (basetype :s= (vl-parse-enum-base-type)))
    (:= (vl-match-token :vl-lcurly))
    (items
       :s= (vl-parse-1+-enum-name-declarations-separated-by-commas))
    (:= (vl-match-token :vl-rcurly))
    (dims := (vl-parse-0+-packed-dimensions))
    (return
         (make-vl-enum :basetype (or basetype
                                     (make-vl-coretype :name :vl-int
                                                       :signedp t))
                       :items items
                       :pdims dims)))
   (type :s= (vl-parse-simple-type))
   (dims := (vl-parse-0+-packed-dimensions))
   (return (vl-datatype-update-pdims dims type)))))

Function: vl-parse-structmembers-fn

(defun vl-parse-structmembers-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-structmembers))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-structmember))
         (when (vl-is-token? :vl-rcurly)
               (return first))
         (rest := (vl-parse-structmembers))
         (return (append first rest)))))

Function: vl-parse-structmember-fn

(defun vl-parse-structmember-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-structmember))
  (declare (ignorable __function__))
  (seq
   tokstream
   (atts :w= (vl-parse-0+-attribute-instances))
   (when (vl-is-some-token? '(:vl-kwd-rand :vl-kwd-randc))
         (rand := (vl-match)))
   (type :s= (vl-parse-datatype-or-void))
   (decls
     := (vl-parse-1+-variable-decl-assignments-separated-by-commas))
   (:= (vl-match-token :vl-semi))
   (unless
    (vl-vardeclassignlist-newfree-p decls)
    (return-raw
     (vl-parse-error
      "Illegal use of 'new' in a struct or union member initial value")))
   (return (let ((rand (and rand
                            (case (vl-token->type rand)
                                  (:vl-kwd-rand :vl-rand)
                                  (:vl-kwd-randc :vl-randc)))))
             (vl-make-structmembers atts rand type decls))))))

Function: vl-parse-variable-dimension-fn

(defun vl-parse-variable-dimension-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-variable-dimension))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when (and (vl-is-token? :vl-lbrack)
              (vl-lookahead-is-token?
                   :vl-rbrack (cdr (vl-tokstream->tokens))))
         (:= (vl-match))
         (:= (vl-match))
         (return (make-vl-dimension-unsized)))
   (when
    (and
        (vl-is-token? :vl-lbrack)
        (vl-lookahead-is-token? :vl-$ (cdr (vl-tokstream->tokens))))
    (ans := (vl-parse-queue-dimension))
    (return ans))
   (return-raw (b* ((backup (vl-tokstream-save))
                    ((mv erp val tokstream)
                     (vl-parse-unpacked-dimension))
                    ((unless erp) (mv erp val tokstream))
                    (tokstream (vl-tokstream-restore backup)))
                 (vl-parse-associative-dimension))))))

Function: vl-parse-associative-dimension-fn

(defun vl-parse-associative-dimension-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-associative-dimension))
    (declare (ignorable __function__))
    (seq tokstream
         (:= (vl-match-token :vl-lbrack))
         (when (vl-is-token? :vl-times)
               (:= (vl-match))
               (:= (vl-match-token :vl-rbrack))
               (return (make-vl-dimension-star)))
         (type := (vl-parse-datatype))
         (:= (vl-match-token :vl-rbrack))
         (return (make-vl-dimension-datatype :type type)))))

Function: vl-parse-0+-variable-dimensions-fn

(defun vl-parse-0+-variable-dimensions-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-0+-variable-dimensions))
    (declare (ignorable __function__))
    (seq tokstream
         (unless (vl-is-token? :vl-lbrack)
                 (return nil))
         (first :s= (vl-parse-variable-dimension))
         (rest := (vl-parse-0+-variable-dimensions))
         (return (cons first rest)))))

Function: vl-parse-variable-decl-assignment-fn

(defun vl-parse-variable-decl-assignment-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-variable-decl-assignment))
    (declare (ignorable __function__))
    (seq tokstream
         (id := (vl-match-token :vl-idtoken))
         (when (vl-is-token? :vl-lbrack)
               (dims :w= (vl-parse-0+-variable-dimensions)))
         (when (vl-is-token? :vl-equalsign)
               (:= (vl-match))
               (rhs := (vl-parse-rhs)))
         (return (make-vl-vardeclassign :id (vl-idtoken->name id)
                                        :dims dims
                                        :rhs rhs)))))

Function: vl-parse-1+-variable-decl-assignments-separated-by-commas-fn

(defun vl-parse-1+-variable-decl-assignments-separated-by-commas-fn
       (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let
  ((__function__
        'vl-parse-1+-variable-decl-assignments-separated-by-commas))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-variable-decl-assignment))
   (when
    (vl-is-token? :vl-comma)
    (:= (vl-match))
    (rest
       :=
       (vl-parse-1+-variable-decl-assignments-separated-by-commas)))
   (return (cons first rest)))))

Function: vl-parse-param-expression-fn

(defun vl-parse-param-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-param-expression))
    (declare (ignorable __function__))
    (b* ((backup (vl-tokstream-save))
         ((mv err expr tokstream)
          (vl-parse-mintypmax-expression))
         ((unless err)
          (mv err (make-vl-paramvalue-expr :expr expr)
              tokstream))
         (tokstream (vl-tokstream-restore backup)))
      (seq tokstream (type := (vl-parse-datatype))
           (return (make-vl-paramvalue-type :type type))))))

Function: vl-parse-named-parameter-assignment-fn

(defun vl-parse-named-parameter-assignment-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-named-parameter-assignment))
   (declare (ignorable __function__))
   (seq tokstream (:= (vl-match-token :vl-dot))
        (id := (vl-match-token :vl-idtoken))
        (:= (vl-match-token :vl-lparen))
        (unless (vl-is-token? :vl-rparen)
                (value := (vl-parse-param-expression)))
        (:= (vl-match-token :vl-rparen))
        (return (make-vl-namedparamvalue :name (vl-idtoken->name id)
                                         :value value)))))

Function: vl-parse-list-of-named-parameter-assignments-fn

(defun vl-parse-list-of-named-parameter-assignments-fn
       (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-list-of-named-parameter-assignments))
  (declare (ignorable __function__))
  (seq
     tokstream
     (first :s= (vl-parse-named-parameter-assignment))
     (when (vl-is-token? :vl-comma)
           (:= (vl-match-token :vl-comma))
           (rest := (vl-parse-list-of-named-parameter-assignments)))
     (return (cons first rest)))))

Function: vl-parse-list-of-ordered-parameter-assignments-fn

(defun vl-parse-list-of-ordered-parameter-assignments-fn
       (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let
   ((__function__ 'vl-parse-list-of-ordered-parameter-assignments))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-param-expression))
   (when (vl-is-token? :vl-comma)
         (:= (vl-match-token :vl-comma))
         (rest := (vl-parse-list-of-ordered-parameter-assignments)))
   (return (cons first rest)))))

Function: vl-parse-list-of-parameter-assignments-fn

(defun vl-parse-list-of-parameter-assignments-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-list-of-parameter-assignments))
  (declare (ignorable __function__))
  (seq
     tokstream
     (when (vl-is-token? :vl-dot)
           (args := (vl-parse-list-of-named-parameter-assignments))
           (return (make-vl-paramargs-named :args args)))
     (exprs :=
            (if (eq (vl-loadconfig->edition config)
                    :verilog-2005)
                (b* (((mv err val tokstream)
                      (vl-parse-1+-expressions-separated-by-commas))
                     ((when err) (mv err nil tokstream)))
                  (mv err (vl-expressions->paramvalues val)
                      tokstream))
              (vl-parse-list-of-ordered-parameter-assignments)))
     (return (make-vl-paramargs-plain :args exprs)))))

Function: vl-parse-parameter-value-assignment-fn

(defun vl-parse-parameter-value-assignment-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-parameter-value-assignment))
  (declare (ignorable __function__))
  (seq
   tokstream
   (:= (vl-match-token :vl-pound))
   (unless
      (vl-is-token? :vl-lparen)
      (expr := (vl-parse-expression))
      (return
           (make-vl-paramargs-plain
                :args (list (make-vl-paramvalue-expr :expr expr)))))
   (:= (vl-match))
   (when (and (vl-is-token? :vl-rparen)
              (not (eq (vl-loadconfig->edition config)
                       :verilog-2005)))
         (:= (vl-match))
         (return (make-vl-paramargs-plain :args nil)))
   (args := (vl-parse-list-of-parameter-assignments))
   (:= (vl-match-token :vl-rparen))
   (return args))))

Function: vl-parse-attr-spec-fn

(defun vl-parse-attr-spec-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-attr-spec))
  (declare (ignorable __function__))
  (seq
   tokstream
   (id := (vl-match-token :vl-idtoken))
   (when (vl-is-token? :vl-equalsign)
         (:= (vl-match))
         (expr := (vl-parse-expression)))
   (when
     (and expr (vl-expr-has-any-atts-p expr))
     (return-raw (vl-parse-error "Nested attributes are illegal.")))
   (return (list (cons (vl-idtoken->name id) expr))))))

Function: vl-parse-attribute-instance-aux-fn

(defun vl-parse-attribute-instance-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-attribute-instance-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (first :s= (vl-parse-attr-spec))
         (when (vl-is-token? :vl-comma)
               (:= (vl-match))
               (rest := (vl-parse-attribute-instance-aux)))
         (return (append first rest)))))

Function: vl-parse-attribute-instance-fn

(defun vl-parse-attribute-instance-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-attribute-instance))
    (declare (ignorable __function__))
    (seq tokstream
         (:= (vl-match-token :vl-beginattr))
         (data := (vl-parse-attribute-instance-aux))
         (:= (vl-match-token :vl-endattr))
         (return data))))

Function: vl-parse-0+-attribute-instances-aux-fn

(defun vl-parse-0+-attribute-instances-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-0+-attribute-instances-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (when (not (vl-is-token? :vl-beginattr))
               (return nil))
         (first :s= (vl-parse-attribute-instance))
         (rest := (vl-parse-0+-attribute-instances-aux))
         (return (append first rest)))))

Function: vl-parse-0+-attribute-instances-fn

(defun vl-parse-0+-attribute-instances-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-0+-attribute-instances))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when (not (vl-is-token? :vl-beginattr))
         (return nil))
   (linestart := (vl-linestart-indent))
   (loc := (vl-current-loc))
   (original-atts := (vl-parse-0+-attribute-instances-aux))
   (return-raw
    (b*
     ((atts (fast-alist-free (hons-shrink-alist (rev original-atts)
                                                nil)))
      ((when (same-lengthp atts original-atts))
       (mv nil atts tokstream))
      (w
       (make-vl-warning
        :type :vl-warn-shadowed-atts
        :msg
        "~l0: Found multiple occurrences of ~&1 in ~
                          attributes.  Later occurrences take precedence."
        :args (list loc
                    (duplicated-members (alist-keys original-atts)))
        :fatalp nil
        :fn __function__))
      (atts (vl-extend-atts-with-linestart linestart atts))
      (tokstream (vl-tokstream-add-warning w)))
     (mv nil atts tokstream))))))

Function: vl-parse-1+-expressions-separated-by-commas-fn

(defun vl-parse-1+-expressions-separated-by-commas-fn
       (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-1+-expressions-separated-by-commas))
  (declare (ignorable __function__))
  (seq
      tokstream
      (first :s= (vl-parse-expression))
      (when (vl-is-token? :vl-comma)
            (:= (vl-match))
            (rest := (vl-parse-1+-expressions-separated-by-commas)))
      (return (cons first rest)))))

Function: vl-parse-patternkey-fn

(defun vl-parse-patternkey-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-patternkey))
    (declare (ignorable __function__))
    (b* (((when (vl-is-token? :vl-kwd-default))
          (seq tokstream (:= (vl-match))
               (return (make-vl-patternkey-default))))
         (backup (vl-tokstream-save))
         ((mv err expr tokstream)
          (vl-parse-expression))
         ((unless err)
          (mv err
              (vl-initial-patternkey-from-expr expr)
              tokstream))
         (tokstream (vl-tokstream-restore backup)))
      (seq tokstream
           (type := (vl-parse-simple-type))
           (return (make-vl-patternkey-type :type type))))))

Function: vl-parse-1+-keyval-expression-pairs-fn

(defun vl-parse-1+-keyval-expression-pairs-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-1+-keyval-expression-pairs))
    (declare (ignorable __function__))
    (seq tokstream
         (key :s= (vl-parse-patternkey))
         (:= (vl-match-token :vl-colon))
         (val :s= (vl-parse-expression))
         (when (vl-is-token? :vl-comma)
               (:= (vl-match))
               (rest := (vl-parse-1+-keyval-expression-pairs)))
         (return (cons (cons key val) rest)))))

Function: vl-parse-expression-without-failure-fn

(defun vl-parse-expression-without-failure-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-expression-without-failure))
    (declare (ignorable __function__))
    (b* ((backup (vl-tokstream-save))
         ((mv err expr tokstream)
          (vl-parse-expression))
         ((unless err) (mv err expr tokstream))
         (tokstream (vl-tokstream-restore backup)))
      (mv nil nil tokstream))))

Function: vl-parse-system-function-call-fn

(defun vl-parse-system-function-call-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-system-function-call))
  (declare (ignorable __function__))
  (seq
   tokstream
   (linestart := (vl-linestart-indent))
   (fn := (vl-match-token :vl-sysidtoken))
   (when (vl-is-token? :vl-lparen)
         (:= (vl-match))
         (arg1 :w= (vl-parse-expression-without-failure))
         (when (and (not arg1)
                    (not (vl-is-token? :vl-rparen)))
               (typearg :w= (vl-parse-simple-type)))
         (when (vl-is-token? :vl-comma)
               (:= (vl-match))
               (args := (vl-parse-sysfuncall-args)))
         (:= (vl-match-token :vl-rparen)))
   (return
    (let ((fname (vl-sysidtoken->name fn)))
     (make-vl-call
      :name
      (make-vl-scopeexpr-end :hid (make-vl-hidexpr-end :name fname))
      :typearg typearg
      :plainargs (if arg1 (cons arg1 args) args)
      :systemp t
      :atts (vl-extend-atts-with-linestart linestart nil)))))))

Function: vl-parse-mintypmax-expression-fn

(defun vl-parse-mintypmax-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-mintypmax-expression))
  (declare (ignorable __function__))
  (seq
   tokstream
   (min :s= (vl-parse-expression))
   (when (vl-is-token? :vl-colon)
         (:= (vl-match))
         (typ :s= (vl-parse-expression))
         (:= (vl-match-token :vl-colon))
         (max := (vl-parse-expression))
         (return (make-vl-mintypmax :min min
                                    :typ typ
                                    :max max)))
   (when (eq (vl-loadconfig->edition config)
             :verilog-2005)
         (return min))
   (linestart1 := (vl-linestart-indent))
   (op := (vl-parse-op 2
                       '((:vl-equalsign . :vl-binary-assign)
                         (:vl-pluseq . :vl-binary-plusassign)
                         (:vl-minuseq . :vl-binary-minusassign)
                         (:vl-timeseq . :vl-binary-timesassign)
                         (:vl-diveq . :vl-binary-divassign)
                         (:vl-remeq . :vl-binary-remassign)
                         (:vl-andeq . :vl-binary-andassign)
                         (:vl-oreq . :vl-binary-orassign)
                         (:vl-xoreq . :vl-binary-xorassign)
                         (:vl-shleq . :vl-binary-shlassign)
                         (:vl-shreq . :vl-binary-shrassign)
                         (:vl-ashleq . :vl-binary-ashlassign)
                         (:vl-ashreq . :vl-binary-ashrassign))))
   (unless op (return min))
   (linestart2 := (vl-linestart-indent))
   (rhs := (vl-parse-expression))
   (return
        (b* ((atts nil)
             (atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (make-vl-binary :op op
                          :left min
                          :right rhs
                          :atts atts))))))

Function: vl-parse-range-expression-fn

(defun vl-parse-range-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-range-expression))
  (declare (ignorable __function__))
  (seq
   tokstream (e1 :s= (vl-parse-expression))
   (unless
       (vl-is-some-token? '(:vl-colon :vl-pluscolon :vl-minuscolon))
       (return (vl-erange :vl-index e1 e1)))
   (sep := (vl-match))
   (e2 := (vl-parse-expression))
   (return (vl-erange (vl-token->type sep)
                      e1 e2)))))

Function: vl-parse-concatenation-fn

(defun vl-parse-concatenation-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-concatenation))
  (declare (ignorable __function__))
  (seq
   tokstream
   (linestart := (vl-linestart-indent))
   (:= (vl-match-token :vl-lcurly))
   (args := (vl-parse-1+-expressions-separated-by-commas))
   (:= (vl-match-token :vl-rcurly))
   (return
       (make-vl-concat
            :parts args
            :atts (vl-extend-atts-with-linestart linestart nil))))))

Function: vl-parse-stream-expression-fn

(defun vl-parse-stream-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-stream-expression))
  (declare (ignorable __function__))
  (seq
   tokstream
   (expr :s= (vl-parse-expression))
   (unless
      (vl-is-token? :vl-kwd-with)
      (return (make-vl-streamexpr :expr expr
                                  :part (make-vl-arrayrange-none))))
   (:= (vl-match))
   (:= (vl-match-token :vl-lbrack))
   (range := (vl-parse-range-expression))
   (:= (vl-match-token :vl-rbrack))
   (return (vl-streamexpr-with expr range)))))

Function: vl-parse-1+-stream-expressions-separated-by-commas-fn

(defun vl-parse-1+-stream-expressions-separated-by-commas-fn
       (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__
            'vl-parse-1+-stream-expressions-separated-by-commas))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-stream-expression))
   (when
     (vl-is-token? :vl-comma)
     (:= (vl-match))
     (rest := (vl-parse-1+-stream-expressions-separated-by-commas)))
   (return (cons first rest)))))

Function: vl-parse-stream-concatenation-fn

(defun vl-parse-stream-concatenation-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-stream-concatenation))
  (declare (ignorable __function__))
  (seq
      tokstream
      (:= (vl-match-token :vl-lcurly))
      (args := (vl-parse-1+-stream-expressions-separated-by-commas))
      (:= (vl-match-token :vl-rcurly))
      (return args))))

Function: vl-parse-pva-tail-fn

(defun vl-parse-pva-tail-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-pva-tail))
  (declare (ignorable __function__))
  (seq
   tokstream
   (:= (vl-match-token :vl-scope))
   (head := (vl-match-token :vl-idtoken))
   (when (vl-is-token? :vl-pound)
         (:= (vl-parse-parameter-value-assignment))
         (return-raw (vl-parse-error "Implement PVAs.")))
   (unless
    (vl-is-token? :vl-scope)
    (return
     (make-vl-scopeexpr-end
         :hid (make-vl-hidexpr-end :name (vl-idtoken->name head)))))
   (tail := (vl-parse-pva-tail))
   (return (make-vl-scopeexpr-colon :first (vl-idtoken->name head)
                                    :rest tail)))))

Function: vl-parse-simple-type-fn

(defun vl-parse-simple-type-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-simple-type))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when
    (vl-is-token? :vl-kwd-local)
    (:= (vl-match))
    (:= (vl-match-token :vl-scope))
    (tail := (vl-match-token :vl-idtoken))
    (return
     (make-vl-usertype
      :name
      (make-vl-scopeexpr-colon
       :first :vl-local
       :rest
       (make-vl-scopeexpr-end
            :hid
            (make-vl-hidexpr-end :name (vl-idtoken->name tail)))))))
   (when
        (vl-is-token? :vl-$unit)
        (:= (vl-match))
        (tail := (vl-parse-pva-tail))
        (return (make-vl-usertype
                     :name (make-vl-scopeexpr-colon :first :vl-$unit
                                                    :rest tail))))
   (unless (vl-is-token? :vl-idtoken)
           (return-raw (vl-parse-very-simple-type)))
   (when
     (vl-lookahead-is-token? :vl-pound (cdr (vl-tokstream->tokens)))
     (:= (vl-match))
     (:= (vl-parse-parameter-value-assignment))
     (return-raw (vl-parse-error "Implement PVAs.")))
   (when
    (vl-lookahead-is-token? :vl-scope (cdr (vl-tokstream->tokens)))
    (head := (vl-match))
    (tail := (vl-parse-pva-tail))
    (return
     (make-vl-usertype
       :name (make-vl-scopeexpr-colon :first (vl-idtoken->name head)
                                      :rest tail))))
   (hid := (vl-parse-hierarchical-identifier nil))
   (return
       (make-vl-usertype :name (make-vl-scopeexpr-end :hid hid))))))

Function: vl-parse-slice-size-fn

(defun vl-parse-slice-size-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-slice-size))
    (declare (ignorable __function__))
    (b* ((backup (vl-tokstream-save))
         ((mv err expr tokstream)
          (vl-parse-expression))
         ((unless err)
          (mv err (make-vl-slicesize-expr :expr expr)
              tokstream))
         (tokstream (vl-tokstream-restore backup)))
      (seq tokstream
           (type := (vl-parse-simple-type))
           (return (make-vl-slicesize-type :type type))))))

Function: vl-parse-any-sort-of-concatenation-aux-fn

(defun vl-parse-any-sort-of-concatenation-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-any-sort-of-concatenation-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (linestart := (vl-linestart-indent))
   (:= (vl-match-token :vl-lcurly))
   (when
       (and (vl-is-token? :vl-rcurly)
            (not (eq (vl-loadconfig->edition config)
                     :verilog-2005)))
       (:= (vl-match))
       (return (vl-expr-update-atts
                    (make-vl-special :key :vl-emptyqueue)
                    (vl-extend-atts-with-linestart linestart nil))))
   (when
    (and (vl-is-some-token? '(:vl-shl :vl-shr))
         (not (eq (vl-loadconfig->edition config)
                  :verilog-2005)))
    (op := (vl-match))
    (unless (vl-is-token? :vl-lcurly)
            (slicesize :s= (vl-parse-slice-size)))
    (args := (vl-parse-stream-concatenation))
    (:= (vl-match-token :vl-rcurly))
    (return
      (b* ((dir (vl-token->type op)))
        (make-vl-stream
             :dir (if (eq dir :vl-shl) :left :right)
             :size (or slicesize (make-vl-slicesize-none))
             :parts args
             :atts (vl-extend-atts-with-linestart linestart nil)))))
   (e1 :s= (vl-parse-expression))
   (when
    (vl-is-token? :vl-lcurly)
    (:= (vl-match))
    (parts := (vl-parse-1+-expressions-separated-by-commas))
    (:= (vl-match-token :vl-rcurly))
    (:= (vl-match-token :vl-rcurly))
    (return
         (make-vl-multiconcat
              :reps e1
              :parts parts
              :atts (vl-extend-atts-with-linestart linestart nil))))
   (when
    (vl-is-token? :vl-comma)
    (:= (vl-match))
    (rest := (vl-parse-1+-expressions-separated-by-commas))
    (:= (vl-match-token :vl-rcurly))
    (return
         (make-vl-concat
              :parts (cons e1 rest)
              :atts (vl-extend-atts-with-linestart linestart nil))))
   (:= (vl-match-token :vl-rcurly))
   (return
       (make-vl-concat
            :parts (list e1)
            :atts (vl-extend-atts-with-linestart linestart nil))))))

Function: vl-parse-any-sort-of-concatenation-fn

(defun vl-parse-any-sort-of-concatenation-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-any-sort-of-concatenation))
  (declare (ignorable __function__))
  (seq
   tokstream
   (concat :s= (vl-parse-any-sort-of-concatenation-aux))
   (when
    (vl-is-token? :vl-lbrack)
    (:= (vl-match))
    (range := (vl-parse-range-expression))
    (:= (vl-match-token :vl-rbrack))
    (return
     (b* (((vl-erange range)))
      (case
       range.type
       (:vl-index (make-vl-bitselect-expr :subexp concat
                                          :index range.left))
       (:vl-colon
        (make-vl-partselect-expr
           :subexp concat
           :part
           (vl-range->partselect (make-vl-range :msb range.left
                                                :lsb range.right))))
       (otherwise
        (make-vl-partselect-expr
            :subexp concat
            :part
            (vl-plusminus->partselect
                 (make-vl-plusminus
                      :base range.left
                      :width range.right
                      :minusp (eq range.type :vl-minuscolon)))))))))
   (return concat))))

Function: vl-parse-hierarchical-identifier-fn

(defun vl-parse-hierarchical-identifier-fn
       (recursivep tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-hierarchical-identifier))
  (declare (ignorable __function__))
  (b* ((sys-p (not (eq (vl-loadconfig->edition config)
                       :verilog-2005))))
   (seq
    tokstream
    (when
     (and sys-p (not recursivep)
          (vl-is-token? :vl-$root))
     (:= (vl-match))
     (:= (vl-match-token :vl-dot))
     (tail := (vl-parse-hierarchical-identifier t))
     (return
      (make-vl-hidexpr-dot :first (make-vl-hidindex :name :vl-$root)
                           :rest tail)))
    (id := (vl-match-token :vl-idtoken))
    (when
     (vl-is-token? :vl-dot)
     (:= (vl-match))
     (tail :s= (vl-parse-hierarchical-identifier t))
     (return
          (make-vl-hidexpr-dot
               :first (make-vl-hidindex :name (vl-idtoken->name id))
               :rest tail)))
    (unless
     sys-p
     (when (vl-is-token? :vl-lbrack)
           (expr :=
                 (b* ((backup (vl-tokstream-save))
                      ((mv err expr tokstream)
                       (seq tokstream (:= (vl-match))
                            (expr :s= (vl-parse-expression))
                            (:= (vl-match-token :vl-rbrack))
                            (:= (vl-match-token :vl-dot))
                            (return expr)))
                      ((unless err) (mv nil expr tokstream))
                      (tokstream (vl-tokstream-restore backup)))
                   (mv nil nil tokstream))))
     (when
      expr
      (tail := (vl-parse-hierarchical-identifier t))
      (return
           (make-vl-hidexpr-dot
                :first (make-vl-hidindex :name (vl-idtoken->name id)
                                         :indices (list expr))
                :rest tail)))
     (return (make-vl-hidexpr-end :name (vl-idtoken->name id))))
    (when
      (vl-is-token? :vl-lbrack)
      (exprs
           :w=
           (b* ((backup (vl-tokstream-save))
                ((mv err exprs tokstream)
                 (seq tokstream
                      (exprs := (vl-parse-0+-bracketed-expressions))
                      (:= (vl-match-token :vl-dot))
                      (return exprs)))
                ((unless err) (mv nil exprs tokstream))
                (tokstream (vl-tokstream-restore backup)))
             (mv nil nil tokstream))))
    (when
      exprs
      (tail := (vl-parse-hierarchical-identifier t))
      (return
           (make-vl-hidexpr-dot
                :first (make-vl-hidindex :name (vl-idtoken->name id)
                                         :indices exprs)
                :rest tail)))
    (return (make-vl-hidexpr-end :name (vl-idtoken->name id)))))))

Function: vl-parse-scoped-hid-fn

(defun vl-parse-scoped-hid-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-scoped-hid))
    (declare (ignorable __function__))
    (b* ((backup (vl-tokstream-save))
         ((mv err first tokstream)
          (seq tokstream (name := (vl-parse-scopename))
               (when (vl-is-some-token? '(:vl-pound :vl-scope))
                     (return name))
               (return-raw (vl-parse-error "backup for hid"))))
         ((when err)
          (b* ((tokstream (vl-tokstream-restore backup)))
            (seq tokstream
                 (hid := (vl-parse-hierarchical-identifier nil))
                 (return (make-vl-scopeexpr-end :hid hid))))))
      (seq tokstream
           (when (vl-is-token? :vl-pound)
                 (params :s= (vl-parse-parameter-value-assignment)))
           (:= (vl-match-token :vl-scope))
           (rest := (vl-parse-scoped-hid))
           (return (make-vl-scopeexpr-colon :first first
                                            :paramargs params
                                            :rest rest))))))

Function: vl-parse-call-namedarg-pair-fn

(defun vl-parse-call-namedarg-pair-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-call-namedarg-pair))
    (declare (ignorable __function__))
    (seq tokstream (:= (vl-match-token :vl-dot))
         (id := (vl-match-token :vl-idtoken))
         (:= (vl-match-token :vl-lparen))
         (unless (vl-is-token? :vl-rparen)
                 (expr :s= (vl-parse-expression)))
         (:= (vl-match-token :vl-rparen))
         (return (cons (vl-idtoken->name id) expr)))))

Function: vl-parse-call-namedargs-aux-fn

(defun vl-parse-call-namedargs-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-call-namedargs-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (unless (vl-is-token? :vl-comma)
                 (return nil))
         (:= (vl-match))
         (pair :s= (vl-parse-call-namedarg-pair))
         (rest := (vl-parse-call-namedargs-aux))
         (return (cons pair rest)))))

Function: vl-parse-call-namedargs-fn

(defun vl-parse-call-namedargs-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-call-namedargs))
    (declare (ignorable __function__))
    (seq tokstream
         (when (vl-is-token? :vl-rparen)
               (return nil))
         (pair :s= (vl-parse-call-namedarg-pair))
         (rest := (vl-parse-call-namedargs-aux))
         (return (cons pair rest)))))

Function: vl-parse-call-plainargs-aux-fn

(defun vl-parse-call-plainargs-aux-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-call-plainargs-aux))
    (declare (ignorable __function__))
    (seq tokstream
         (unless (vl-is-token? :vl-comma)
                 (return nil))
         (:= (vl-match))
         (when (vl-is-token? :vl-rparen)
               (return (list nil)))
         (when (vl-is-token? :vl-dot)
               (return nil))
         (unless (vl-is-token? :vl-comma)
                 (expr :s= (vl-parse-expression)))
         (rest := (vl-parse-call-plainargs-aux))
         (return (cons expr rest)))))

Function: vl-parse-call-plainargs-fn

(defun vl-parse-call-plainargs-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-call-plainargs))
    (declare (ignorable __function__))
    (seq tokstream
         (when (vl-is-token? :vl-dot)
               (return nil))
         (unless (vl-is-token? :vl-comma)
                 (expr :s= (vl-parse-expression)))
         (rest := (vl-parse-call-plainargs-aux))
         (return (cons expr rest)))))

Function: vl-parse-function-call-fn

(defun vl-parse-function-call-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-function-call))
  (declare (ignorable __function__))
  (seq
   tokstream
   (linestart := (vl-linestart-indent))
   (id :s= (vl-parse-scoped-hid))
   (atts :w= (vl-parse-0+-attribute-instances))
   (:= (vl-match-token :vl-lparen))
   (when
    (and (not (eq (vl-loadconfig->edition config)
                  :verilog-2005))
         (vl-is-token? :vl-rparen))
    (:= (vl-match-token :vl-rparen))
    (return
        (make-vl-call
             :name id
             :systemp nil
             :atts (vl-extend-atts-with-linestart linestart atts))))
   (plainargs :w= (vl-parse-call-plainargs))
   (namedargs :w= (vl-parse-call-namedargs))
   (:= (vl-match-token :vl-rparen))
   (return
      (make-vl-call
           :name id
           :plainargs plainargs
           :namedargs namedargs
           :systemp nil
           :atts (vl-extend-atts-with-linestart linestart atts))))))

Function: vl-parse-0+-bracketed-expressions-fn

(defun vl-parse-0+-bracketed-expressions-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-0+-bracketed-expressions))
   (declare (ignorable __function__))
   (b*
     (((unless (vl-plausible-start-of-range-p))
       (mv nil nil tokstream))
      (backup (vl-tokstream-save))
      ((mv err first tokstream)
       (seq tokstream (:= (vl-match))
            (expr := (vl-parse-expression))
            (:= (vl-match-token :vl-rbrack))
            (return expr)))
      ((when (or err (not first)))
       (b* ((tokstream (vl-tokstream-restore backup)))
         (mv nil nil tokstream)))
      ((unless (mbt (< (vl-tokstream-measure)
                       (len (vl-tokstream-backup->tokens backup)))))
       (raise "termination failure")
       (vl-parse-error "termination failure"))
      ((mv erp rest tokstream)
       (vl-parse-0+-bracketed-expressions))
      ((when erp) (mv erp rest tokstream)))
     (mv nil (cons first rest) tokstream))))

Function: vl-parse-indexed-id-2005-fn

(defun vl-parse-indexed-id-2005-fn
       (scopes recursivep tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (declare (xargs :guard (vl-scopenamelist-p scopes)))
 (let ((__function__ 'vl-parse-indexed-id-2005))
  (declare (ignorable __function__))
  (seq
   tokstream
   (hid :s= (vl-parse-hierarchical-identifier recursivep))
   (bexprs :w= (vl-parse-0+-bracketed-expressions))
   (when (vl-plausible-start-of-range-p)
         (:= (vl-match))
         (range := (vl-parse-range-expression))
         (:= (vl-match-token :vl-rbrack)))
   (return (let* ((ans (vl-tack-scopes-onto-hid scopes hid)))
             (if range (vl-build-range-select ans bexprs range)
               (make-vl-index :scope ans
                              :indices bexprs
                              :part (make-vl-partselect-none))))))))

Function: vl-parse-indexed-id-2012-fn

(defun vl-parse-indexed-id-2012-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-indexed-id-2012))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when
    (vl-is-some-token? '(:vl-kwd-local :vl-$unit))
    (first := (vl-match))
    (:= (vl-match-token :vl-scope))
    (morescopes := (vl-parse-0+-scope-prefixes))
    (return-raw
     (vl-parse-indexed-id-2005 (cons (case (vl-token->type first)
                                           (:vl-kwd-local :vl-local)
                                           (:vl-$unit :vl-$unit))
                                     morescopes)
                               t)))
   (scopes := (vl-parse-0+-scope-prefixes))
   (return-raw (vl-parse-indexed-id-2005 scopes (consp scopes))))))

Function: vl-parse-indexed-id-fn

(defun vl-parse-indexed-id-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-indexed-id))
    (declare (ignorable __function__))
    (seq tokstream
         (linestart := (vl-linestart-indent))
         (ans :=
              (if (eq (vl-loadconfig->edition config)
                      :verilog-2005)
                  (vl-parse-indexed-id-2005 nil nil)
                (vl-parse-indexed-id-2012)))
         (return (vl-extend-expr-with-linestart linestart ans)))))

Function: vl-parse-assignment-pattern-fn

(defun vl-parse-assignment-pattern-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-assignment-pattern))
  (declare (ignorable __function__))
  (b* ((backup (vl-tokstream-save))
       ((mv expr-err first-expr tokstream)
        (seq tokstream
             (expr :w= (vl-parse-expression))
             (return expr)))
       ((mv err first-key tokstream)
        (if expr-err (b* ((tokstream (vl-tokstream-restore backup)))
                       (seq tokstream
                            (key :w= (vl-parse-patternkey))
                            (return key)))
          (mv nil
              (vl-initial-patternkey-from-expr first-expr)
              tokstream)))
       ((when err) (mv err nil tokstream)))
   (seq
    tokstream
    (when
       (vl-is-token? :vl-colon)
       (:= (vl-match))
       (firstval :s= (vl-parse-expression))
       (when (vl-is-token? :vl-rcurly)
             (:= (vl-match))
             (return (make-vl-assignpat-keyval
                          :pairs (list (cons first-key firstval)))))
       (:= (vl-match-token :vl-comma))
       (rest := (vl-parse-1+-keyval-expression-pairs))
       (:= (vl-match-token :vl-rcurly))
       (return (make-vl-assignpat-keyval
                    :pairs (cons (cons first-key firstval) rest))))
    (when expr-err
          (return-raw (mv expr-err nil tokstream)))
    (when
       (vl-is-token? :vl-rcurly)
       (:= (vl-match))
       (return
            (make-vl-assignpat-positional :vals (list first-expr))))
    (when
     (vl-is-token? :vl-comma)
     (:= (vl-match))
     (rest := (vl-parse-1+-expressions-separated-by-commas))
     (:= (vl-match-token :vl-rcurly))
     (return
       (make-vl-assignpat-positional :vals (cons first-expr rest))))
    (:= (vl-match-token :vl-lcurly))
    (parts := (vl-parse-1+-expressions-separated-by-commas))
    (:= (vl-match-token :vl-rcurly))
    (:= (vl-match-token :vl-rcurly))
    (return (make-vl-assignpat-repeat :reps first-expr
                                      :vals parts))))))

Function: vl-parse-primary-main-fn

(defun vl-parse-primary-main-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-primary-main))
  (declare (ignorable __function__))
  (b*
   ((backup (vl-tokstream-save))
    ((mv errmsg? expr tokstream)
     (vl-maybe-parse-base-primary))
    ((when (or errmsg? expr))
     (mv errmsg? expr tokstream))
    (tokstream (vl-tokstream-restore backup))
    (tokens (vl-tokstream->tokens))
    ((when (atom tokens))
     (vl-parse-error "Unexpected EOF."))
    (type (vl-token->type (car tokens)))
    ((when (or (eq type :vl-idtoken)
               (eq type :vl-$root)
               (eq type :vl-$unit)
               (eq type :vl-kwd-local)))
     (b* (((mv err funcall tokstream)
           (vl-parse-function-call))
          ((unless err)
           (mv err funcall tokstream))
          (tokstream (vl-tokstream-restore backup)))
       (vl-parse-indexed-id)))
    ((when (eq type :vl-lcurly))
     (vl-parse-any-sort-of-concatenation))
    ((when (eq type :vl-sysidtoken))
     (vl-parse-system-function-call))
    ((when (eq type :vl-lparen))
     (seq tokstream (:= (vl-match))
          (expr := (vl-parse-mintypmax-expression))
          (:= (vl-match-token :vl-rparen))
          (return (vl-mark-as-explicit-parens expr))))
    ((when (eq type :vl-quote))
     (seq
      tokstream
      (linestart := (vl-linestart-indent))
      (:= (vl-match))
      (:= (vl-match-token :vl-lcurly))
      (pat := (vl-parse-assignment-pattern))
      (return
       (make-vl-pattern
            :pat pat
            :atts (vl-extend-atts-with-linestart linestart nil))))))
   (vl-parse-error "Failed to match a primary expression."))))

Function: vl-parse-primary-cast-fn

(defun vl-parse-primary-cast-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-primary-cast))
  (declare (ignorable __function__))
  (seq
   tokstream
   (primary :s= (vl-parse-primary-main))
   (when
    (vl-is-token? :vl-quote)
    (:= (vl-match))
    (when
     (vl-is-token? :vl-lparen)
     (:= (vl-match))
     (arg := (vl-parse-expression))
     (:= (vl-match-token :vl-rparen))
     (return (make-vl-cast :to (make-vl-casttype-size :size primary)
                           :expr arg)))
    (:= (vl-match-token :vl-lcurly))
    (pattern := (vl-parse-assignment-pattern))
    (return-raw
     (b* ((type (vl-interpret-expr-as-type primary))
          ((unless type)
           (vl-parse-error
                "Couldn't interpret cast expression as datatype.")))
       (mv nil
           (make-vl-pattern :pattype type
                            :pat pattern)
           tokstream))))
   (return primary))))

Function: vl-parse-nonprimary-cast-fn

(defun vl-parse-nonprimary-cast-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-nonprimary-cast))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when
    (vl-is-some-token?
         '(:vl-kwd-signed :vl-kwd-unsigned
                          :vl-kwd-string :vl-kwd-const))
    (type := (vl-match))
    (:= (vl-match-token :vl-quote))
    (:= (vl-match-token :vl-lparen))
    (arg := (vl-parse-expression))
    (:= (vl-match-token :vl-rparen))
    (return
     (b*
      ((casting-type
        (case
           (vl-token->type type)
           (:vl-kwd-signed (make-vl-casttype-signedness :signedp t))
           (:vl-kwd-unsigned
                (make-vl-casttype-signedness :signedp nil))
           (:vl-kwd-string
                (make-vl-casttype-type
                     :type (make-vl-coretype :name :vl-string)))
           (:vl-kwd-const (make-vl-casttype-const)))))
      (make-vl-cast :to casting-type
                    :expr arg))))
   (type :s= (vl-parse-simple-type))
   (:= (vl-match-token :vl-quote))
   (:= (vl-match-token :vl-lparen))
   (arg := (vl-parse-expression))
   (:= (vl-match-token :vl-rparen))
   (return (make-vl-cast :to (make-vl-casttype-type :type type)
                         :expr arg)))))

Function: vl-parse-primary-fn

(defun vl-parse-primary-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-primary))
    (declare (ignorable __function__))
    (b* (((when (eq (vl-loadconfig->edition config)
                    :verilog-2005))
          (vl-parse-primary-main))
         (backup (vl-tokstream-save))
         ((mv errmsg expr tokstream)
          (vl-parse-primary-cast))
         ((unless errmsg)
          (mv errmsg expr tokstream))
         (tokstream (vl-tokstream-restore backup))
         ((mv errmsg expr tokstream)
          (vl-parse-nonprimary-cast))
         ((unless errmsg)
          (mv errmsg expr tokstream))
         (tokstream (vl-tokstream-restore backup)))
      (vl-parse-error "Failed to match a primary expression."))))

Function: vl-parse-unary-expression-fn

(defun vl-parse-unary-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-unary-expression))
  (declare (ignorable __function__))
  (seq
   tokstream
   (linestart := (vl-linestart-indent))
   (op :=
       (if (eq (vl-loadconfig->edition config)
               :verilog-2005)
           (vl-parse-op 1
                        '((:vl-plus . :vl-unary-plus)
                          (:vl-minus . :vl-unary-minus)
                          (:vl-lognot . :vl-unary-lognot)
                          (:vl-bitnot . :vl-unary-bitnot)
                          (:vl-bitand . :vl-unary-bitand)
                          (:vl-nand . :vl-unary-nand)
                          (:vl-bitor . :vl-unary-bitor)
                          (:vl-nor . :vl-unary-nor)
                          (:vl-xor . :vl-unary-xor)
                          (:vl-xnor . :vl-unary-xnor)))
         (vl-parse-op 1
                      '((:vl-plus . :vl-unary-plus)
                        (:vl-minus . :vl-unary-minus)
                        (:vl-lognot . :vl-unary-lognot)
                        (:vl-bitnot . :vl-unary-bitnot)
                        (:vl-bitand . :vl-unary-bitand)
                        (:vl-nand . :vl-unary-nand)
                        (:vl-bitor . :vl-unary-bitor)
                        (:vl-nor . :vl-unary-nor)
                        (:vl-xor . :vl-unary-xor)
                        (:vl-xnor . :vl-unary-xnor)
                        (:vl-plusplus . :vl-unary-preinc)
                        (:vl-minusminus . :vl-unary-predec)))))
   (unless
    op (primary :s= (vl-parse-primary))
    (when (eq (vl-loadconfig->edition config)
              :verilog-2005)
          (return primary))
    (return-raw
     (b*
      ((backup (vl-tokstream-save))
       ((mv err val tokstream)
        (seq
         tokstream
         (atts := (vl-parse-0+-attribute-instances))
         (post
           := (vl-parse-op 1
                           '((:vl-plusplus . :vl-unary-postinc)
                             (:vl-minusminus . :vl-unary-postdec))))
         (unless post (return nil))
         (return
          (vl-expr-update-atts (make-vl-unary :op post :arg primary)
                               atts))))
       ((when (and (not err) val))
        (mv nil val tokstream))
       (tokstream (vl-tokstream-restore backup)))
      (mv nil primary tokstream))))
   (atts :w= (vl-parse-0+-attribute-instances))
   (primary :=
            (if (member-eq op '(:vl-unary-lognot :vl-unary-bitnot))
                (vl-parse-unary-expression)
              (vl-parse-primary)))
   (return (make-vl-unary
                :op op
                :atts (vl-extend-atts-with-linestart linestart atts)
                :arg primary)))))

Function: vl-parse-power-expression-aux-fn

(defun vl-parse-power-expression-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-power-expression-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-unary-expression))
   (unless (vl-is-token? :vl-power)
           (return (list first)))
   (linestart1 := (vl-linestart-indent))
   (:= (vl-match))
   (linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (tail := (vl-parse-power-expression-aux))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list* first :vl-binary-power atts tail))))))

Function: vl-parse-power-expression-fn

(defun vl-parse-power-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-power-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-power-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-mult-expression-aux-fn

(defun vl-parse-mult-expression-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-mult-expression-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-power-expression))
   (linestart1 := (vl-linestart-indent))
   (op := (vl-parse-op 2
                       '((:vl-times . :vl-binary-times)
                         (:vl-div . :vl-binary-div)
                         (:vl-rem . :vl-binary-rem))))
   (unless op (return (list first)))
   (linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (tail := (vl-parse-mult-expression-aux))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list* first op atts tail))))))

Function: vl-parse-mult-expression-fn

(defun vl-parse-mult-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-mult-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-mult-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-add-expression-aux-fn

(defun vl-parse-add-expression-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-add-expression-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-mult-expression))
   (linestart1 := (vl-linestart-indent))
   (op := (vl-parse-op 2
                       '((:vl-plus . :vl-binary-plus)
                         (:vl-minus . :vl-binary-minus))))
   (unless op (return (list first)))
   (linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (tail := (vl-parse-add-expression-aux))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list* first op atts tail))))))

Function: vl-parse-add-expression-fn

(defun vl-parse-add-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-add-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-add-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-shift-expression-aux-fn

(defun vl-parse-shift-expression-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-shift-expression-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-add-expression))
   (linestart1 := (vl-linestart-indent))
   (op := (vl-parse-op 2
                       '((:vl-shl . :vl-binary-shl)
                         (:vl-shr . :vl-binary-shr)
                         (:vl-ashl . :vl-binary-ashl)
                         (:vl-ashr . :vl-binary-ashr))))
   (unless op (return (list first)))
   (linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (tail := (vl-parse-shift-expression-aux))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list* first op atts tail))))))

Function: vl-parse-shift-expression-fn

(defun vl-parse-shift-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-shift-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-shift-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-compare-expression-aux-fn

(defun vl-parse-compare-expression-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-compare-expression-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-shift-expression))
   (when
    (vl-is-token? :vl-kwd-inside)
    (linestart1 := (vl-linestart-indent))
    (:= (vl-match))
    (linestart2 := (vl-linestart-indent))
    (:= (vl-match-token :vl-lcurly))
    (set := (vl-parse-1+-open-value-ranges))
    (:= (vl-match-token :vl-rcurly))
    (return
        (b* ((atts nil)
             (atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list (make-vl-inside :elem first
                                :set set
                                :atts atts)))))
   (linestart1 := (vl-linestart-indent))
   (op := (vl-parse-op 2
                       '((:vl-lt . :vl-binary-lt)
                         (:vl-lte . :vl-binary-lte)
                         (:vl-gt . :vl-binary-gt)
                         (:vl-gte . :vl-binary-gte))))
   (unless op (return (list first)))
   (linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (tail := (vl-parse-compare-expression-aux))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list* first op atts tail))))))

Function: vl-parse-compare-expression-fn

(defun vl-parse-compare-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-compare-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-compare-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-open-value-range-fn

(defun vl-parse-open-value-range-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-open-value-range))
    (declare (ignorable __function__))
    (seq tokstream
         (when (vl-plausible-start-of-range-p)
               (:= (vl-match))
               (low :w= (vl-parse-expression))
               (:= (vl-match-token :vl-colon))
               (high := (vl-parse-expression))
               (:= (vl-match-token :vl-rbrack))
               (return (make-vl-valuerange-range :low low
                                                 :high high)))
         (expr := (vl-parse-expression))
         (return (make-vl-valuerange-single :expr expr)))))

Function: vl-parse-1+-open-value-ranges-fn

(defun vl-parse-1+-open-value-ranges-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-1+-open-value-ranges))
    (declare (ignorable __function__))
    (seq tokstream
         (range1 :s= (vl-parse-open-value-range))
         (when (vl-is-token? :vl-comma)
               (:= (vl-match))
               (rest := (vl-parse-1+-open-value-ranges)))
         (return (cons range1 rest)))))

Function: vl-parse-equality-expression-aux-fn

(defun vl-parse-equality-expression-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-equality-expression-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-compare-expression))
   (linestart1 := (vl-linestart-indent))
   (op := (vl-parse-op 2
                       '((:vl-eq . :vl-binary-eq)
                         (:vl-neq . :vl-binary-neq)
                         (:vl-ceq . :vl-binary-ceq)
                         (:vl-cne . :vl-binary-cne)
                         (:vl-wildeq . :vl-binary-wildeq)
                         (:vl-wildneq . :vl-binary-wildneq))))
   (unless op (return (list first)))
   (linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (tail := (vl-parse-equality-expression-aux))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list* first op atts tail))))))

Function: vl-parse-equality-expression-fn

(defun vl-parse-equality-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-equality-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-equality-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-bitand-expression-aux-fn

(defun vl-parse-bitand-expression-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-bitand-expression-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-equality-expression))
   (unless (vl-is-token? :vl-bitand)
           (return (list first)))
   (linestart1 := (vl-linestart-indent))
   (:= (vl-match))
   (linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (tail := (vl-parse-bitand-expression-aux))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list* first :vl-binary-bitand atts tail))))))

Function: vl-parse-bitand-expression-fn

(defun vl-parse-bitand-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-bitand-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-bitand-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-bitxor-expression-aux-fn

(defun vl-parse-bitxor-expression-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-bitxor-expression-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-bitand-expression))
   (linestart1 := (vl-linestart-indent))
   (op := (vl-parse-op 2
                       '((:vl-xor . :vl-binary-xor)
                         (:vl-xnor . :vl-binary-xnor))))
   (linestart2 := (vl-linestart-indent))
   (unless op (return (list first)))
   (atts :w= (vl-parse-0+-attribute-instances))
   (tail := (vl-parse-bitxor-expression-aux))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list* first op atts tail))))))

Function: vl-parse-bitxor-expression-fn

(defun vl-parse-bitxor-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-bitxor-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-bitxor-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-bitor-expression-aux-fn

(defun vl-parse-bitor-expression-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-bitor-expression-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-bitxor-expression))
   (unless (vl-is-token? :vl-bitor)
           (return (list first)))
   (linestart1 := (vl-linestart-indent))
   (:= (vl-match))
   (linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (tail := (vl-parse-bitor-expression-aux))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list* first :vl-binary-bitor atts tail))))))

Function: vl-parse-bitor-expression-fn

(defun vl-parse-bitor-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-bitor-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-bitor-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-logand-expression-aux-fn

(defun vl-parse-logand-expression-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-logand-expression-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-bitor-expression))
   (unless (vl-is-token? :vl-logand)
           (return (list first)))
   (linestart1 := (vl-linestart-indent))
   (:= (vl-match))
   (linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (tail := (vl-parse-logand-expression-aux))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list* first :vl-binary-logand atts tail))))))

Function: vl-parse-logand-expression-fn

(defun vl-parse-logand-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-logand-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-logand-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-logor-expression-aux-fn

(defun vl-parse-logor-expression-aux-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-logor-expression-aux))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-logand-expression))
   (unless (vl-is-token? :vl-logor)
           (return (list first)))
   (linestart1 := (vl-linestart-indent))
   (:= (vl-match))
   (linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (tail := (vl-parse-logor-expression-aux))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (list* first :vl-binary-logor atts tail))))))

Function: vl-parse-logor-expression-fn

(defun vl-parse-logor-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-logor-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (mixed := (vl-parse-logor-expression-aux))
         (return (vl-left-associate-mixed-binop-list mixed)))))

Function: vl-parse-qmark-expression-fn

(defun vl-parse-qmark-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-qmark-expression))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-logor-expression))
   (unless (vl-is-token? :vl-qmark)
           (return first))
   (qmark-linestart1 := (vl-linestart-indent))
   (:= (vl-match))
   (qmark-linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (second :s= (vl-parse-expression))
   (colon-linestart1 := (vl-linestart-indent))
   (:= (vl-match-token :vl-colon))
   (colon-linestart2 := (vl-linestart-indent))
   (third := (vl-parse-qmark-expression))
   (return
       (b* ((qmark-linestart (or qmark-linestart1 qmark-linestart2))
            (colon-linestart (or colon-linestart1 colon-linestart2))
            (atts (if qmark-linestart
                      (cons (hons "VL_QMARK_LINESTART"
                                  (vl-make-index qmark-linestart))
                            atts)
                    atts))
            (atts (if colon-linestart
                      (cons (hons "VL_COLON_LINESTART"
                                  (vl-make-index colon-linestart))
                            atts)
                    atts)))
         (make-vl-qmark :test first
                        :then second
                        :else third
                        :atts atts))))))

Function: vl-parse-impl-expression-fn

(defun vl-parse-impl-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-impl-expression))
  (declare (ignorable __function__))
  (seq
   tokstream
   (first :s= (vl-parse-qmark-expression))
   (when (eq (vl-loadconfig->edition config)
             :verilog-2005)
         (return first))
   (linestart1 := (vl-linestart-indent))
   (op := (vl-parse-op 2
                       '((:vl-arrow . :vl-implies)
                         (:vl-equiv . :vl-equiv))))
   (unless op (return first))
   (linestart2 := (vl-linestart-indent))
   (atts :w= (vl-parse-0+-attribute-instances))
   (second :s= (vl-parse-impl-expression))
   (return
        (b* ((atts (vl-extend-atts-with-linestart linestart2 atts))
             (atts (vl-extend-atts-with-linestart linestart1 atts)))
          (make-vl-binary :op op
                          :left first
                          :right second
                          :atts atts))))))

Function: vl-parse-event-expression-2005-fn

(defun vl-parse-event-expression-2005-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-event-expression-2005))
  (declare (ignorable __function__))
  (seq tokstream
       (when (vl-is-some-token? '(:vl-kwd-posedge :vl-kwd-negedge))
             (edge := (vl-match)))
       (expr :s= (vl-parse-expression))
       (when (vl-is-some-token? '(:vl-kwd-or :vl-comma))
             (:= (vl-match))
             (rest := (vl-parse-event-expression-2005)))
       (return (let ((edgetype (if (not edge)
                                   :vl-noedge
                                 (case (vl-token->type edge)
                                       (:vl-kwd-posedge :vl-posedge)
                                       (:vl-kwd-negedge :vl-negedge)
                                       (t (impossible))))))
                 (cons (make-vl-evatom :type edgetype
                                       :expr expr)
                       rest))))))

Function: vl-parse-event-expression-2012-fn

(defun vl-parse-event-expression-2012-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-event-expression-2012))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when (vl-is-token? :vl-lparen)
         (:= (vl-match))
         (nested :w= (vl-parse-event-expression-2012))
         (:= (vl-match-token :vl-rparen)))
   (unless nested
           (edge :w= (vl-parse-optional-edge-identifier))
           (expr :s= (vl-parse-expression)))
   (when
    (vl-is-token? :vl-kwd-iff)
    (return-raw
     (vl-parse-error
      "BOZO need to implement event_expressions with 'iff' clauses.")))
   (when (vl-is-some-token? '(:vl-kwd-or :vl-comma))
         (:= (vl-match))
         (rest := (vl-parse-event-expression-2012)))
   (return (if nested (append-without-guard nested rest)
             (cons (make-vl-evatom :type edge :expr expr)
                   rest))))))

Function: vl-parse-event-expression-fn

(defun vl-parse-event-expression-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-event-expression))
    (declare (ignorable __function__))
    (seq tokstream
         (when (eq (vl-loadconfig->edition config)
                   :verilog-2005)
               (ret := (vl-parse-event-expression-2005))
               (return ret))
         (ret := (vl-parse-event-expression-2012))
         (return ret))))

Function: vl-parse-clocking-event-fn

(defun vl-parse-clocking-event-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-clocking-event))
  (declare (ignorable __function__))
  (seq
   tokstream
   (:= (vl-match-token :vl-atsign))
   (when
    (vl-is-token? :vl-idtoken)
    (id := (vl-match))
    (return
     (list
         (make-vl-evatom :type :vl-noedge
                         :expr (vl-idexpr (vl-idtoken->name id))))))
   (:= (vl-match-token :vl-lparen))
   (evatoms := (vl-parse-event-expression))
   (:= (vl-match-token :vl-rparen))
   (return evatoms))))

Function: vl-parse-expr-or-clocking-event-fn

(defun vl-parse-expr-or-clocking-event-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-expr-or-clocking-event))
    (declare (ignorable __function__))
    (seq tokstream
         (when (vl-is-token? :vl-atsign)
               (evatoms := (vl-parse-clocking-event))
               (return (make-vl-eventexpr :atoms evatoms)))
         (expr := (vl-parse-expression))
         (return expr))))

Function: vl-parse-sysfuncall-args-fn

(defun vl-parse-sysfuncall-args-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-sysfuncall-args))
    (declare (ignorable __function__))
    (seq tokstream
         (when (vl-is-token? :vl-rparen)
               (return nil))
         (when (vl-is-token? :vl-comma)
               (:= (vl-match))
               (rest := (vl-parse-sysfuncall-args))
               (return (cons nil rest)))
         (first :s= (vl-parse-expr-or-clocking-event))
         (when (vl-is-token? :vl-comma)
               (:= (vl-match))
               (rest := (vl-parse-sysfuncall-args)))
         (return (cons first rest)))))

Function: vl-parse-expression-fn

(defun vl-parse-expression-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-expression))
  (declare (ignorable __function__))
  (seq
   tokstream
   (unless (and (vl-is-token? :vl-kwd-tagged)
                (not (eq (vl-loadconfig->edition config)
                         :verilog-2005)))
           (expr :s= (vl-parse-impl-expression))
           (return expr))
   (linestart := (vl-linestart-indent))
   (:= (vl-match))
   (id := (vl-match-token :vl-idtoken))
   (return-raw
    (b*
     ((tag (vl-idtoken->name id))
      (atts (vl-extend-atts-with-linestart linestart nil))
      (backup (vl-tokstream-save))
      ((mv err expr tokstream)
       (seq tokstream
            (expr :s= (vl-parse-expression))
            (return expr)))
      ((when err)
       (b* ((tokstream (vl-tokstream-restore backup)))
         (mv nil (make-vl-tagged :tag tag :atts atts)
             tokstream)))
      ((unless (or (hons-assoc-equal "VL_EXPLICIT_PARENS"
                                     (vl-expr->atts expr))
                   (vl-expr-case expr
                                 :vl-binary nil
                                 :vl-qmark nil
                                 :otherwise t)))
       (vl-parse-error
        "Cowardly refusing to support tagged union expression such as
                   'tagged foo 1 + 2' due to unclear precedence.  Workaround:
                   add explicit parens, e.g., write 'tagged foo (1 + 2)'
                   instead."))
      (ans (make-vl-tagged :tag tag
                           :expr expr
                           :atts atts)))
     (mv nil ans tokstream))))))

Subtopics

Vl-expressions->paramvalues
(vl-expressions->paramvalues x) maps vl-paramvalue-expr across a list.
Vl-erange-p
An expression range is a temporary internal representation of the ranges for select-like expressions (bit selects, array indexes, part selects, +: and -: expressions.
Vl-mixed-binop-list-p
A list of alternating expressions, operators, and attributes.
Vl-parse-very-simple-type
Match the very simplest simple_type keywords, return an expression.
Vl-parse-0+-scope-prefixes
Match { id '::' } and return a list of all the ids that have been matched.
Vl-parse-0+-attribute-instances
Top level parser for { attribute_instance } with proper duplicity checking and warnings. Returns a vl-atts-p.
Vl-parse-hierarchical-identifier
Match a hierarchical_identifier.
Vl-parse-op
Compatible with seq. Match any of the tokens specified in this alist, and return the corresponding vl-op-p for it.
Vl-mark-as-explicit-parens
Annotate an expression as having explicit parentheses.
Vl-parse-expression-top
Vl-parse-any-sort-of-concatenation-aux
Match single, multiple, or streaming concatenations, or empty queues.
Vl-parse-datatype-or-implicit
Vl-vardeclassignlist-p
(vl-vardeclassignlist-p x) recognizes lists where every element satisfies vl-vardeclassign-p.
Vl-build-range-select
Vl-parse-scopename
Vl-parse-optional-edge-identifier
Vl-make-structmembers
Vl-erangetypelist-p
(vl-erangetypelist-p x) recognizes lists where every element satisfies vl-erangetype-p.
Vl-coretypekwd->info
Find the properties (vl-coredatatype-info structure) for a coretype by its token name (for parsing).
Vl-streamexpr-with
Vl-parse-simple-type
Match simple_type and return an expression.
Vl-expr-has-any-atts-p
Check whether an expression has any attributes.
Vl-vardeclassignlist-newfree-p
Vl-tack-scopes-onto-hid
Vl-left-associate-mixed-binop-list
Vl-extend-atts-with-linestart
Vl-parse-op-alist-p
Vl-make-guts-from-inttoken
Vl-extend-expr-with-linestart
Vl-interpret-expr-as-type
Vl-initial-patternkey-from-expr
Vl-parse-range-expression
Match range_expression, returning an vl-erange-p.
Vl-parse-slice-size
Match slice_size ::= simple_type | expression and return it as an expression.
Vl-parse-concatenation
Match concatenation ::= '{' expression { ',' expression } '}' and return a single :vl-concat expression.
Vl-parse-stream-expression
Match stream_expression, returning a single expression.
Vl-plausible-start-of-range-p
Vl-parse-any-sort-of-concatenation
Match single, multiple, or streaming concatenations, perhaps with a bit/partselect.
Vl-parse-1+-stream-expressions-separated-by-commas
Match at least one (but perhaps more) stream expressions, return them as an expression list.
Vl-parse-stream-concatenation
Match stream_concatenation, return an expression list.
Vl-parse-primary
Vl-parse-datatype
Vl-parse-0+-bracketed-expressions
Match { '[' expression '] }'), return an expression list.
Vl-parse-variable-decl-assignment
Vl-parse-system-function-call
Vl-parse-shift-expression-aux
Vl-parse-power-expression-aux
Vl-parse-parameter-value-assignment
Vl-parse-named-parameter-assignment
Vl-parse-mult-expression-aux
Vl-parse-mintypmax-expression
Vl-parse-logor-expression-aux
Vl-parse-logand-expression-aux
Vl-parse-list-of-parameter-assignments
Vl-parse-indexed-id-2012
Vl-parse-indexed-id-2005
Vl-parse-expression-without-failure
Vl-parse-expr-or-clocking-event
Vl-parse-event-expression-2012
Vl-parse-event-expression-2005
Vl-parse-event-expression
Vl-parse-equality-expression-aux
Vl-parse-equality-expression
Vl-parse-enum-name-declaration
Vl-parse-compare-expression-aux
Vl-parse-bitxor-expression-aux
Vl-parse-bitor-expression-aux
Vl-parse-bitand-expression-aux
Vl-parse-associative-dimension
Vl-parse-1+-variable-decl-assignments-separated-by-commas
Vl-parse-1+-open-value-ranges
Vl-parse-1+-keyval-expression-pairs
Vl-parse-1+-enum-name-declarations-separated-by-commas
Vl-parse-0+-variable-dimensions
Vl-parse-0+-unpacked-dimensions
Vl-parse-0+-packed-dimensions
Vl-parse-variable-dimension
Vl-parse-unpacked-dimension
Vl-parse-unary-expression
Vl-parse-sysfuncall-args
Vl-parse-structmembers
Vl-parse-structmember
Vl-parse-shift-expression
Vl-parse-scoped-hid
Vl-parse-rhs
Vl-parse-range
Vl-parse-queue-dimension
Vl-parse-qmark-expression
Vl-parse-pva-tail
Vl-parse-primary-main
Vl-parse-primary-cast
Vl-parse-power-expression
Vl-parse-patternkey
Vl-parse-param-expression
Vl-parse-packeddimension
Vl-parse-open-value-range
Vl-parse-nonprimary-cast
Vl-parse-mult-expression
Vl-parse-logor-expression
Vl-parse-logand-expression
Vl-parse-list-of-ordered-parameter-assignments
Vl-parse-list-of-named-parameter-assignments
Vl-parse-indexed-id
Vl-parse-impl-expression
Vl-parse-function-call
Vl-parse-expression
Vl-parse-enum-base-type
Vl-parse-datatype-or-void
Vl-parse-core-data-type
Vl-parse-compare-expression
Vl-parse-clocking-event
Vl-parse-call-plainargs-aux
Vl-parse-call-plainargs
Vl-parse-call-namedargs-aux
Vl-parse-call-namedargs
Vl-parse-call-namedarg-pair
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
Vl-parse-0+-ranges