• 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-timetoken
                • Make-vl-timetoken
                • Change-vl-timetoken
                • Make-honsed-vl-timetoken
                • Honsed-vl-timetoken
                • Vl-timetoken->units
                • Vl-timetoken->quantity
                • Vl-timetoken->etext
                • Vl-timetoken->breakp
              • 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-timetoken-p

Tokens for time literals, like 3ns or 45.617us.

(vl-timetoken-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)).
  • quantity — An ACL2 string with the amount. In practice, the amount should match either unsigned_number or fixed_point_number, e.g., "3" or "45.617". We don't try to process this further because (1) we don't expect it to matter for much, and (2) ACL2 doesn't really support fixed point numbers.
        Invariant (stringp quantity).
  • units — The kind of time unit this is, e.g., seconds, milliseconds, microseconds, ...
        Invariant (vl-timeunit-p units).
  • breakp — Was this the first token on a line.
        Invariant (booleanp breakp).

Source link: vl-timetoken-p

Subtopics

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