• 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
            • Lex-strings
            • Lex-identifiers
            • Vl-typo-uppercase-p
            • Vl-typo-number-p
            • Vl-typo-lowercase-p
            • Lex-numbers
            • Chartypes
            • Vl-lex
            • Defchar
            • Tokens
              • Vl-tokentype-p
              • Vl-inttoken-p
              • Vl-plaintoken-p
              • Vl-token->etext
              • Vl-token-p
              • Vl-idtoken-p
              • Vl-token->type
              • Vl-timetoken-p
              • Vl-stringtoken-p
                • Vl-stringtoken
                • Make-vl-stringtoken
                • Change-vl-stringtoken
                • Make-honsed-vl-stringtoken
                • Honsed-vl-stringtoken
                • Vl-stringtoken->expansion
                • Vl-stringtoken->etext
                • Vl-stringtoken->breakp
              • Vl-sysidtoken-p
              • Vl-extinttoken-p
              • Vl-realtoken-p
              • Vl-kill-whitespace-and-comments
              • Vl-tokenlist->etext
              • Vl-tokenlist-p
              • Vl-tokenlist->string-with-spaces
              • Vl-idtoken-list-p
              • Vl-tokentypelist-p
              • Vl-token->breakp
              • Vl-token->loc
              • Vl-plaintokentypelist-p
              • Vl-tokenlistlist-p
              • Vl-token->string
            • Lex-keywords
            • Lexstate
            • Make-test-tokens
            • Lexer-utils
            • Lex-comments
            • Vl-typo-uppercase-list-p
            • Vl-typo-lowercase-list-p
            • Vl-typo-number-list-p
          • Parser
          • 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
  • Tokens

Vl-stringtoken-p

Tokens for string literals.

(vl-stringtoken-p x) is a defaggregate of the following fields.

  • etext — The characters that gave rise to this string literal from the Verilog source. Note that this text is "verbatim" and, as a consequence, character sequences like \n will not have been converted into newlines, etc.
        Invariant (and (vl-echarlist-p etext) (consp etext)).
  • expansion — An ordinary ACL2 string object that holds the "expanded" version of the string literal. That is, character sequences like \n in the etext become real newline characters in the expansion.
        Invariant (stringp expansion).
  • breakp — Was this the first token on a line.
        Invariant (booleanp breakp).

Source link: vl-stringtoken-p

The expansion is carried out per Table 3-1, on page 14 of the Verilog-2005 standard. BOZO is that still valid for SystemVerilog?

Subtopics

Vl-stringtoken
Raw constructor for vl-stringtoken-p structures.
Make-vl-stringtoken
Constructor macro for vl-stringtoken-p structures.
Change-vl-stringtoken
A copying macro that lets you create new vl-stringtoken-p structures, based on existing structures.
Make-honsed-vl-stringtoken
Constructor macro for honsed vl-stringtoken-p structures.
Honsed-vl-stringtoken
Raw constructor for honsed vl-stringtoken-p structures.
Vl-stringtoken->expansion
Access the expansion field of a vl-stringtoken-p structure.
Vl-stringtoken->etext
Access the etext field of a vl-stringtoken-p structure.
Vl-stringtoken->breakp
Access the breakp field of a vl-stringtoken-p structure.