(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?
