• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Mlib

Vl-parse-expr-from-str

Try to parse a Verilog expression from an ACL2 string.

It is occasionally convenient to parse Verilog expressions from strings, for instance in ACL2::symbolic-test-vectors we want to let the user write Verilog-style hierarchical identifiers to describe the wires they are interested in.

(vl-parse-expr-from-str str) returns a vl-expr-p or nil to signal failure.

We expect that str contains exactly one Verilog expression. We will fail if this isn't the case, or if any part of the lexing/parsing process fails or produces warnings. In these cases we will print warning messages to standard output, but there's no programmatic way to extract the warnings.

We have arbitrarily decided not to preprocess the string. This means you can't use `ifdef stuff or `defines. However, comments and whitespace are tolerated and ignored.

We don't transform the expression at all. This means, for instance, that if you parse an expression like "foo[3-1:0]" then it'll still have the subtract there. Furthermore, we don't know what module the expression belongs in, so it won't be sized, may refer to invalid wires, etc.

Definitions and Theorems

Function: vl-parse-expr-from-str

(defun vl-parse-expr-from-str (str)
 (declare (xargs :guard (stringp str)))
 (b*
  ((echars (vl-echarlist-from-str str))
   ((mv successp tokens warnings)
    (vl-lex echars
            :config *vl-default-loadconfig*
            :warnings nil))
   ((unless successp)
    (cw "; vl-parse-expr-from-str: Lexing failed for ~s0.~%"
        str))
   ((when warnings)
    (vl-cw-ps-seq
         (vl-println "Warnings from VL-PARSE-EXPR-FROM-STR:")
         (vl-print-warnings warnings))
    (cw "; vl-parse-expr-from-str: Lexer warnings for ~s0.~%"
        str))
   ((mv tokens ?cmap)
    (vl-kill-whitespace-and-comments tokens))
   (pstate (make-vl-parsestate :warnings nil))
   ((local-stobjs tokstream)
    (mv val tokstream))
   (tokstream (vl-tokstream-update-tokens tokens))
   (tokstream (vl-tokstream-update-pstate pstate))
   ((mv err val tokstream)
    (vl-parse-expression :config *vl-default-loadconfig*))
   ((when err)
    (vl-report-parse-error err tokens)
    (cw "; vl-parse-expr-from-str: Parsing failed for ~s0.~%"
        str)
    (mv nil tokstream))
   ((vl-parsestate pstate)
    (vl-tokstream->pstate))
   ((when pstate.warnings)
    (vl-cw-ps-seq
         (vl-println "Warnings from VL-PARSE-EXPR-FROM-STR:")
         (vl-print-warnings pstate.warnings))
    (cw "; vl-parse-expr-from-str: Parser warnings for ~s0."
        str)
    (mv nil tokstream))
   ((when (vl-tokstream->tokens))
    (cw
     "; vl-parse-expr-from-str: Content remains after parsing an ~
                 expression from the string.~% ~
                 - Original string: ~s0~% ~
                 - First expr: ~s1~% ~
                 - Remaining after parse: ~s2~%"
     str (vl-pps-expr val)
     (vl-tokenlist->string-with-spaces (vl-tokstream->tokens)))
    (mv nil tokstream)))
  (mv val tokstream)))

Theorem: vl-expr-p-of-vl-parse-expr-from-string

(defthm vl-expr-p-of-vl-parse-expr-from-string
  (equal (vl-expr-p (vl-parse-expr-from-str str))
         (if (vl-parse-expr-from-str str)
             t
           nil)))