• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
        • Range-tools
        • Finding-by-name
        • Stmt-tools
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
          • Lvaluecheck
          • Vl-expr-variable-lvalue-p
          • Vl-expr-net-lvalue-p
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Lvalues
• Vl-parse-variable-lvalue-2012

Vl-expr-variable-lvalue-p

Recognize an expression that is OK for a SystemVerilog-2012 variable_lvalue.

Signature

(vl-expr-variable-lvalue-p x) → bool

Arguments

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

Here's the original grammar for variable_lvalue.

variable_lvalue ::= [ implicit_class_handle '.' | package_scope ] hierarchical_variable_identifier select
                  | '{' variable_lvalue { ',' variable_lvalue } '}'
                  | [ assignment_pattern_expression_type ] assignment_pattern_variable_lvalue
                  | streaming_concatenation

Footnote 46 applies. In a variable_lvalue that is assigned within a sequence_match_item, any select shall also be a constant_select. But that's not local to variable_lvalue (and for that matter isn't really a syntactic requirement anyway), so we don't check that here.

Footnote 47 also applies. The streaming_concatenation expression here shall not be nested within another variable_lvalue, shall not be the target of an increment or decrement operator, nor the target of any assignment operator except the simple = or nonblocking assignment <= operator. It's easy for us to rule out nested streaming concatenations here, but the remaining requirements aren't local to variable_lvalue so we don't check them here.

The first production essentially corresponds to our notion of an index expression, the second to concatenation. The third production is quite similar to assignment_pattern_expression, which can be a valid expression primary,

assignment_pattern_expression ::= [ assignment_pattern_expression_type ] assignment_pattern

Except that here we have an assignment_pattern_variable_lvalue instead of an assignment_pattern. So let's compare:

assignment_pattern_variable_lvalue ::= QUOTE '{' variable_lvalue { ',' variable_lvalue } '}'

assignment_pattern ::= QUOTE '{' expression { ',' expression } '}'
                     | QUOTE '{' structure_pattern_key ...
                     | QUOTE '{' array_pattern_key ...
                     | QUOTE '{' constant_expression '{' ...

So essentially the grammar is just trying to (1) rule out the fancier structure/array/replication assignment patterns while still allowing basic positional assignment patterns, and (2) ensure that all of the expressions within the assignment pattern here happen to be good variable_lvalues. We'll recognize these expressions with vl-expr-variable-lvalue-p.

Finally, the last production just corresponds to our usual notion of streaming concatenation, modulo the nesting restriction, so that's about it.

Comparing all of the above to the story for net_lvalue, I think these are exactly the same as net_lvalue except that we allow streaming concatenations.

Definitions and Theorems

Function: vl-expr-variable-lvalue-p

(defun vl-expr-variable-lvalue-p (x)
  (declare (xargs :guard (vl-expr-p x)))
  (let ((__function__ 'vl-expr-variable-lvalue-p))
    (declare (ignorable __function__))
    (let ((x (vl-expr-fix x)))
      (or (vl-expr-net-lvalue-p x)
          (vl-expr-case x :vl-stream)))))

Theorem: vl-expr-variable-lvalue-p-of-vl-expr-fix-x

(defthm vl-expr-variable-lvalue-p-of-vl-expr-fix-x
  (equal (vl-expr-variable-lvalue-p (vl-expr-fix x))
         (vl-expr-variable-lvalue-p x)))

Theorem: vl-expr-variable-lvalue-p-vl-expr-equiv-congruence-on-x

(defthm vl-expr-variable-lvalue-p-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-expr-variable-lvalue-p x)
                  (vl-expr-variable-lvalue-p x-equiv)))
  :rule-classes :congruence)