• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Vwsim
      • Fgl
      • Vl
        • Syntax
          • Vl-module
          • Vl-vardecl
          • Vl-fundecl
          • Vl-interface
          • Vl-design
          • Vl-assign
          • Vl-modinst
          • Vl-gateinst
          • Vl-taskdecl
          • Vl-portdecl
          • Vl-commentmap
          • Vl-dpiimport
          • Vl-ansi-portdecl
          • Vl-package
          • Vl-paramdecl
          • Vl-dpiexport
          • Vl-class
          • Vl-sort-blockitems-aux
          • Vl-plainarglist->exprs
          • Vl-taskdecllist->names
          • Expressions-and-datatypes
            • Vl-atts
            • Vl-expr
              • Vl-expr-p
              • Vl-expr->atts
              • Vl-index
              • Vl-call
              • Vl-exprsign
              • Vl-maybe-expr
              • Vl-stream
              • Vl-expr-case
              • Vl-pattern
              • Vl-literal
                • Vl-value
                  • Vl-constint
                  • Vl-weirdint
                  • Vl-value-fix
                  • Vl-value-p
                  • Vl-value-case
                  • Vl-time
                    • Vl-time->units
                    • Vl-time->quantity
                    • Make-vl-time
                    • Change-vl-time
                    • Vl-timeunit
                  • Vl-real
                  • Vl-extint
                  • Vl-value-equiv
                  • Vl-string
                  • Vl-value-kind
                  • Vl-valuelist
                • Vl-literal->val
                • Vl-literal->atts
                • Make-vl-literal
                • Change-vl-literal
              • Vl-binary
              • Vl-expr-update-atts
              • Vl-unary
              • Vl-special
              • Vl-qmark
              • Vl-inside
              • Vl-cast
              • Vl-multiconcat
              • Vl-mintypmax
              • Vl-tagged
              • Vl-concat
              • Vl-expr-equiv
              • Vl-eventexpr
              • Vl-expr-kind
              • Vl-exprlist
              • Vl-maybe-exprlist
              • Vl-expr-fix
              • Vl-expr-count
            • Vl-datatype
            • New-expression-representation
            • Vl-paramargs
            • Vl-evatom
            • Vl-maybe-paramargs
            • Vl-evatomlist
            • Vl-call-namedargs
            • Vl-paramvaluelist
            • Vl-namedparamvaluelist
          • Vl-fundecllist->names
          • Vl-udp
          • Vl-port
          • Vl-genelement
          • Vl-clkdecl
          • Vl-parse-temps
          • Vl-bind
          • Vl-namedarg
          • Vl-exprdist
          • Vl-clkassign
          • Vl-range
          • Vl-propport
          • Vl-typedef
          • Vl-gatedelay
          • Vl-dimension
          • Vl-sequence
          • Vl-clkskew
          • Vl-program
          • Vl-gatestrength
          • Vl-property
          • Vl-config
          • Vl-always
          • Vl-import
          • Vl-repeateventcontrol
          • Vl-timeliteral
          • Vl-initial
          • Vl-eventcontrol
          • Vl-final
          • Vl-udpsymbol-p
          • Vl-maybe-clkskew
          • Vl-alias
          • Vl-maybe-nettypename
          • Vl-maybe-gatedelay
          • Vl-letdecl
          • Vl-direction-p
          • Vl-modelement
          • Vl-maybe-timeprecisiondecl
          • Vl-maybe-scopeid
          • Vl-maybe-gatestrength
          • Vl-maybe-direction
          • Vl-maybe-delayoreventcontrol
          • Vl-gclkdecl
          • Vl-fwdtypedef
          • Vl-maybe-udpsymbol-p
          • Vl-maybe-timeunitdecl
          • Vl-maybe-timeliteral
          • Vl-maybe-parse-temps
          • Vl-maybe-cstrength
          • Vl-arguments
          • Vl-maybe-module
          • Vl-maybe-design
          • Vl-covergroup
          • Vl-udpline
          • Vl-timeunitdecl
          • Vl-genvar
          • Vl-defaultdisable
          • Vl-context1
          • Vl-timeprecisiondecl
          • Vl-sort-blockitems
          • Vl-elabtask
          • Vl-udpedge
          • Vl-delaycontrol
          • Vl-context
          • Vl-ctxelement
          • Vl-ctxelement->loc
          • Vl-modelement->loc
          • Statements
          • Vl-blockitem
          • Vl-vardecllist
          • Vl-interface->ifports
          • Vl-syntaxversion
          • Vl-nettypename-p
          • Vl-module->ifports
          • Vl-lifetime-p
          • Vl-paramdecllist
          • Vl-modelementlist->genelements
          • Vl-importlist
          • Vl-typedeflist
          • Vl-gatetype-p
          • Vl-cstrength-p
          • Vl-port->name
          • Vl-genelement->loc
          • Vl-delayoreventcontrol
          • Vl-udpentry-p
          • Vl-portdecllist
          • Vl-elabtask->loc
          • Property-expressions
          • Vl-taskdecllist
          • Vl-port->loc
          • Vl-fundecllist
          • Vl-sequencelist
          • Vl-propertylist
          • Vl-portlist
          • Vl-dpiimportlist
          • Vl-dpiexportlist
          • Vl-classlist
          • Vl-arguments->args
          • Vl-alwaystype-p
          • Vl-modinstlist
          • Vl-importpart-p
          • Vl-importpart-fix
          • Vl-bindlist
          • Vl-initiallist
          • Vl-genvarlist
          • Vl-gclkdecllist
          • Vl-finallist
          • Vl-elabtasklist
          • Vl-defaultdisablelist
          • Vl-clkdecllist
          • Vl-cassertionlist
          • Vl-blockstmt-p
          • Vl-assignlist
          • Vl-assertionlist
          • Vl-alwayslist
          • Vl-aliaslist
          • Vl-udptable
          • Vl-udplist
          • Vl-udpentrylist
          • Vl-propportlist
          • Vl-programlist
          • Vl-packagelist
          • Vl-namedarglist
          • Vl-modulelist
          • Vl-modportlist
          • Vl-modport-portlist
          • Vl-letdecllist
          • Vl-interfacelist
          • Vl-gateinstlist
          • Vl-fwdtypedeflist
          • Vl-covergrouplist
          • Vl-configlist
          • Vl-clkassignlist
          • Vl-blockitemlist
          • Vl-ansi-portdecllist
          • Vl-regularportlist
          • Vl-paramdecllist-list
          • Vl-modelementlist
          • Vl-interfaceportlist
          • Vl-casekey-p
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
      • Svl
      • X86isa
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Vl-value

Vl-time

Representation of time amounts like 45.12ns.

This is a product type, introduced by deftagsum in support of vl-value.

Fields
quantity — stringp
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.
units — vl-timeunit-p
The kind of time unit this is, e.g., seconds, milliseconds, microseconds, ...

We barely support this. You should probably not rely on our current representation, since we will almost certainly want to change it as soon as we do anything with time units.

Subtopics

Vl-time->units
Get the units field from a vl-time.
Vl-time->quantity
Get the quantity field from a vl-time.
Make-vl-time
Basic constructor macro for vl-time structures.
Change-vl-time
Modifying constructor for vl-time structures.
Vl-timeunit
Representation for SystemVerilog time units (s, ms, ps, ...).