• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
            • Parse-udps
            • Parse-statements
            • Parse-property
              • Vl-parse-property-list-of-arguments
              • Vl-parse-sequence-match-item
              • Vl-parse-property-actual-arg
                • Vl-parse-scoped-or-hierarchical-identifier
                • Vl-parse-cycledelayrange
                • Vl-parse-sequence-abbrev
                • Vl-parse-boolean-abbrev
                • Vl-parse-1+-expression-or-dists-separated-by-commas
                • Vl-parse-property-acceptop
                • Vl-parse-dist-item
                • Vl-parse-sequence-match-item-list
                • Vl-parse-property-spec
                • Vl-parse-impl-prop-expr-op
                • Vl-parse-expression-or-dist
                • Vl-parse-dist-list
                • Vl-alternating-propexpr/op-list-p
                • Vl-left-associate-alternating-propexpr/op-list
                • Vl-left-associate-delay-se-tail
                • Vl-delay-se-tail-p
                • Vl-parse-1+-named-property-list-of-arguments
                • Vl-parse-property-low-prec-unary
                • Vl-parse-within-sequence-expr-aux
                • Vl-parse-throughout-sequence-expr
                • Vl-parse-or-property-expr-aux
                • Vl-parse-intersect-sequence-expr-aux
                • Vl-parse-intersect-sequence-expr
                • Vl-parse-delay-sequence-expr
                • Vl-parse-assign-sequence-expr
                • Vl-parse-and-property-expr-aux
                • Vl-parse-1+-property-case-items
                • Vl-parse-within-sequence-expr
                • Vl-parse-or-property-expr
                • Vl-parse-instance-property-expr
                • Vl-parse-iff-property-expr
                • Vl-parse-delay-sequence-expr-tail
                • Vl-parse-and-property-expr
                • Vl-parse-until-property-expr
                • Vl-parse-strength-property-expr
                • Vl-parse-repeat-sequence-expr
                • Vl-parse-property-expr
                • Vl-parse-property-case-item
                • Vl-parse-not-property-expr
                • Vl-parse-impl-property-expr
                • Vl-parse-firstmatch-sequence-expr
              • 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
    • Parse-property

    Vl-parse-property-actual-arg

    Match a single sequence_actual_arg.

    Signature
    (vl-parse-property-actual-arg name &key (tokstream 'tokstream) 
                                  (config 'config)) 
     
      → 
    (mv errmsg? value new-tokstream)
    Arguments
    name — Guard (stringp name).
    config — Guard (vl-loadconfig-p config).

    This is used in the special case where we know that we want to match exactly one (perhaps optional) property_actual_arg followed by a right paren, e.g., we are matching bar in .foo(bar) or similar.

    The basic grammar rule here is:

    property_actual_arg ::= property_expr
                          | sequence_actual_arg
    
    sequence_actual_arg ::= event_expression
                          | sequence_expr

    We don't really distinguish between property_expr and sequence_expr. But even without the vast ambiguity between them, this is also ambiguous in a couple of ways.

    First, any ordinary expression is simultaneously an event_expression and also a sequence_expr, e.g., via expression_or_dist. So if we just see an identifier like foo or some other expression, it may be an event expression or a sequence expression, and it isn't clear what we should prefer. Furthermore, the keyword or makes it so that an event expression such as a or b might instead be interpreted as a sequence expression.

    In the special case where we know that we're expecting a single property_actual_arg followed by a right-paren, e.g., .foo(bar), it seems fairly reasonable to just use backtracking to try both possibilities and see which (if any) leads us to the right place. If both succeed, e.g., perhaps bar is an ordinary expression, we arbitrarily choose to prefer a property_expr over an event_expression.