• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
          • Vl-module
          • Vl-vardecl
          • Expressions
            • Vl-atts
            • Vl-constint
            • *vl-ops-table*
            • Vl-weirdint
            • Vl-expr
            • Vl-id
            • Vl-hidpiece
            • Vl-time
            • Vl-maybe-exprtype
            • Vl-op-p
            • Vl-maybe-expr
            • Vl-expr->finaltype
            • Vl-real
              • Vl-real-fix
              • Vl-real-equiv
              • Make-vl-real
              • Change-vl-real
              • Vl-real->value
              • Vl-real-p
            • Vl-expr->finalwidth
            • Vl-tagname
            • Vl-sysfunname
            • Vl-string
            • Vl-op-arity
            • Vl-keyguts
            • Vl-exprtype-p
            • Vl-typename
            • Vl-funname
            • Vl-basictype
            • Vl-extint
            • Vl-atomlist-p
            • Vl-atomguts
            • Vl-nbits-fix
            • Vl-atom-p
            • Vl-arity-fix
            • Vl-arity-ok-p
            • Vl-op-text
            • Vl-exprlist
            • Vl-oplist
            • Vl-exprlistlist
            • Vl-ops-table
            • *vl-default-expr*
          • Vl-fundecl
          • Vl-assign
          • Vl-gateinst
          • Vl-modinst
          • Vl-commentmap
          • Vl-portdecl
          • Vl-taskdecl
          • Vl-design
          • Vl-interface
          • Vl-plainarglist->exprs
          • Vl-taskdecllist->names
          • Vl-fundecllist->names
          • Vl-package
          • Vl-port
          • Vl-udp
          • Vl-paramdecl
          • Vl-genelement
          • Vl-cycledelayrange
          • Vl-namedarg
          • Vl-sort-blockitems-aux
          • Vl-distitem
          • Vl-gatedelay
          • Vl-repetition
          • Vl-typedef
          • Vl-range
          • Vl-gatestrength
          • Vl-program
          • Vl-config
          • Vl-always
          • Vl-datatype-update-dims
          • Vl-import
          • Vl-enumbasetype
          • Vl-repeateventcontrol
          • Vl-paramargs
          • Vl-initial
          • Vl-eventcontrol
          • Vl-udpsymbol-p
          • Vl-maybe-range
          • Vl-maybe-nettypename
          • Vl-maybe-gatestrength
          • Vl-maybe-gatedelay
          • Vl-maybe-delayoreventcontrol
          • Vl-alias
          • Maybe-string-fix
          • Vl-maybe-packeddimension
          • Vl-fwdtypedef
          • Vl-evatom
          • Vl-packeddimension-p
          • Vl-maybe-udpsymbol
          • Vl-maybe-module
          • Vl-maybe-direction
          • Vl-maybe-datatype
          • Vl-maybe-cstrength
          • Vl-direction-p
          • Vl-arguments
          • Vl-maybe-design
          • Vl-udpline
          • Vl-exprdist
          • Vl-context1
          • Vl-genvar
          • Vl-enumitem
          • Vl-datatype-update-udims
          • Vl-datatype-update-pdims
          • Vl-modelement
          • Vl-udpedge
          • Vl-delaycontrol
          • Vl-context
          • Vl-sort-blockitems
          • Vl-distweighttype-p
          • Vl-ctxelement->loc
          • Vl-blockitem
          • Vl-vardecllist
          • Vl-module->ifports
          • Vl-modelement->loc
          • Vl-ctxelement
          • Vl-coretypename-p
          • Vl-packeddimensionlist
          • Vl-modelementlist->genelements
          • Vl-gatetype-p
          • Vl-paramdecllist
          • Vl-lifetime-p
          • Vl-datatype->udims
          • Vl-datatype->pdims
          • Vl-timeunit-p
          • Vl-repetitiontype-p
          • Vl-port->name
          • Vl-importlist
          • Vl-genelement->loc
          • Vl-delayoreventcontrol
          • Vl-cstrength-p
          • Statements
          • Vl-udpentry-p
          • Vl-packeddimension-fix
          • Vl-nettypename-p
          • Vl-portdecllist
          • Vl-port->loc
          • Vl-enumbasekind-fix
          • Vl-arguments->args
          • Vl-taskdecllist
          • Vl-portlist
          • Vl-importpart-p
          • Vl-importpart-fix
          • Vl-fundecllist
          • Vl-blockstmt-p
          • Vl-assignlist
          • Vl-alwaystype-p
          • Vl-typedeflist
          • Vl-syntaxversion-p
          • Vl-randomqualifier-p
          • Vl-modinstlist
          • Vl-gateinstlist
          • Vl-blockitemlist
          • Vl-udptable
          • Vl-udplist
          • Vl-udpentrylist
          • Vl-programlist
          • Vl-paramvaluelist
          • Vl-packagelist
          • Vl-namedparamvaluelist
          • Vl-namedarglist
          • Vl-modulelist
          • Vl-modportlist
          • Vl-modport-portlist
          • Vl-interfacelist
          • Vl-initiallist
          • Vl-genvarlist
          • Vl-fwdtypedeflist
          • Vl-evatomlist
          • Vl-enumitemlist
          • Vl-distlist
          • Vl-configlist
          • Vl-alwayslist
          • Vl-aliaslist
          • Vl-regularportlist
          • Vl-rangelist-list
          • Vl-rangelist
          • Vl-paramdecllist-list
          • Vl-modelementlist
          • Vl-maybe-range-list
          • Vl-interfaceportlist
          • Vl-argumentlist
          • Data-types
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Expressions

Vl-real

Representation of real (floating point) literals.

This is a product type introduced by defprod.

Fields
value — stringp
The actual characters found in the source code, i.e., it might be a string such as "3.41e+12".

We have almost no support for working with real numbers. You should probably not rely on our current representation, since we will almost certainly want to change it as soon as we want to do anything with real numbers.

Subtopics

Vl-real-fix
Fixing function for vl-real structures.
Vl-real-equiv
Basic equivalence relation for vl-real structures.
Make-vl-real
Basic constructor macro for vl-real structures.
Change-vl-real
Modifying constructor for vl-real structures.
Vl-real->value
Get the value field from a vl-real.
Vl-real-p
Recognizer for vl-real structures.