• 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-inttoken
                • Make-vl-inttoken
                • Change-vl-inttoken
                • Honsed-vl-inttoken
                • Vl-inttoken-constraint-p
                • Make-honsed-vl-inttoken
                • Vl-inttoken->width
                • Vl-inttoken->wasunsized
                • Vl-inttoken->value
                • Vl-inttoken->signedp
                • Vl-inttoken->etext
                • Vl-inttoken->breakp
                • Vl-inttoken->bits
              • Vl-plaintoken-p
              • Vl-token->etext
              • Vl-token-p
              • Vl-idtoken-p
              • Vl-token->type
              • Vl-timetoken-p
              • Vl-stringtoken-p
              • 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-inttoken-p

Tokens for integer constants.

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

  • etext — The characters that gave rise to this token.
        Invariant (and (vl-echarlist-p etext) (consp etext)).
  • width — The width of this integer. Note that VL acts like a 32-bit Verilog implementation and, for an unsized integer like 3 or 'b101 we will produce a 32-bit token. See also some additional discussion in vl-constint.
        Invariant (posp width).
  • signedp — Whether this number is to be treated as a signed value. This is decided by in Section 3.5.1, and for instance 19 is signed, 'd19 is unsigned, 'sd19 is signed, and so on.
        Invariant (booleanp signedp).
  • value — nil when there are any X or Z digits. Otherwise, a natural number that reflects the actual value of this constant. Note that there are no negative numbers because, e.g., -5 basically is interpreted as a unary-minus operator applied to 5.
        Invariant (maybe-natp value).
  • bits — nil unless there are any X or Z digits. In these cases, it is a msb-first vl-bitlist that contains exactly width-many bits.
        Invariant (vl-bitlist-p bits).
  • wasunsized — Indicates whether the constant was originally unsized. If so, VL acts like a 32-bit implementation and the resulting integer will have width 32. Mainly intended for use in linting or other kinds of heuristic checking. See also vl-constint and vl-weirdint.
        Invariant (booleanp wasunsized).
  • breakp — Was this the first token on a line.
        Invariant (booleanp breakp).

Source link: vl-inttoken-p

Subtopics

Vl-inttoken
Raw constructor for vl-inttoken-p structures.
Make-vl-inttoken
Constructor macro for vl-inttoken-p structures.
Change-vl-inttoken
A copying macro that lets you create new vl-inttoken-p structures, based on existing structures.
Honsed-vl-inttoken
Raw constructor for honsed vl-inttoken-p structures.
Vl-inttoken-constraint-p
Basic well-formedness constraint on integer tokens.
Make-honsed-vl-inttoken
Constructor macro for honsed vl-inttoken-p structures.
Vl-inttoken->width
Access the width field of a vl-inttoken-p structure.
Vl-inttoken->wasunsized
Access the wasunsized field of a vl-inttoken-p structure.
Vl-inttoken->value
Access the value field of a vl-inttoken-p structure.
Vl-inttoken->signedp
Access the signedp field of a vl-inttoken-p structure.
Vl-inttoken->etext
Access the etext field of a vl-inttoken-p structure.
Vl-inttoken->breakp
Access the breakp field of a vl-inttoken-p structure.
Vl-inttoken->bits
Access the bits field of a vl-inttoken-p structure.