• 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
          • 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-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-function-specialization
          • 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-propexpr
              • Vl-propexpr-p
              • Vl-propthen
              • Vl-propexpr-case
              • Vl-propbinary
              • Vl-propeventually
              • Vl-propassign
              • Vl-propalways
              • Vl-propif
              • Vl-propaccept
              • Vl-proprepeat
              • Vl-propnexttime
              • Vl-propclock
              • Vl-propexpr-equiv
              • Vl-propunary
              • Vl-propinst
              • Vl-propexpr-kind
              • Vl-propthroughout
              • Vl-propcase
              • Vl-propcore
              • *vl-trivially-true-property-expr*
              • Vl-propexpr-fix
              • Vl-propexpr-count
            • Vl-propspec
            • Vl-propactual
            • Vl-propcaseitem
            • Vl-propcaseitemlist
            • Vl-propactuallist
          • 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-function-specialization-map
          • 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
          • Sv::maybe-4veclist
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Property-expressions

Vl-propexpr

Representation of a single property or sequence expression.

This is a tagged union type, introduced by deftagsum.

Member Tags → Types
:vl-propcore → vl-propcore
Basic, single expression in a sequence or property (perhaps with some probability distribution stuff.)
:vl-propinst → vl-propinst
Instance of a named sequence or property.
:vl-propthen → vl-propthen
Sequential sequence composition, i.e., foo ##1 bar and similar.
:vl-proprepeat → vl-proprepeat
A sequence with repetitions.
:vl-propassign → vl-propassign
A sequence with sequence match items (updates to its variables).
:vl-propthroughout → vl-propthroughout
A throughout sequence expression.
:vl-propclock → vl-propclock
A sequence or property expression with a clocking event.
:vl-propunary → vl-propunary
A basic unary operator applied to a sequence/property, for instance, like first_match(a), not(b), etc.
:vl-propbinary → vl-propbinary
A basic binary operator that joins two sequences/properties, like a and b, a |-> b, etc.
:vl-propalways → vl-propalways
An always or s_always property expression.
:vl-propeventually → vl-propeventually
An eventually or s_eventually property expression.
:vl-propaccept → vl-propaccept
A (possibly synchronous) accept_on or reject_on property expression.
:vl-propnexttime → vl-propnexttime
A nexttime or s_nexttime property expression.
:vl-propif → vl-propif
An if-else property expression.
:vl-propcase → vl-propcase
A case property expression.

Note that SystemVerilog distinguishes between properties and sequences. However, VL internally represents both property and sequence expressions using this same data structure.

Subtopics

Vl-propexpr-p
Recognizer for vl-propexpr structures.
Vl-propthen
Sequential sequence composition, i.e., foo ##1 bar and similar.
Vl-propexpr-case
Case macro for the different kinds of vl-propexpr structures.
Vl-propbinary
A basic binary operator that joins two sequences/properties, like a and b, a |-> b, etc.
Vl-propeventually
An eventually or s_eventually property expression.
Vl-propassign
A sequence with sequence match items (updates to its variables).
Vl-propalways
An always or s_always property expression.
Vl-propif
An if-else property expression.
Vl-propaccept
A (possibly synchronous) accept_on or reject_on property expression.
Vl-proprepeat
A sequence with repetitions.
Vl-propnexttime
A nexttime or s_nexttime property expression.
Vl-propclock
A sequence or property expression with a clocking event.
Vl-propexpr-equiv
Basic equivalence relation for vl-propexpr structures.
Vl-propunary
A basic unary operator applied to a sequence/property, for instance, like first_match(a), not(b), etc.
Vl-propinst
Instance of a named sequence or property.
Vl-propexpr-kind
Get the kind (tag) of a vl-propexpr structure.
Vl-propthroughout
A throughout sequence expression.
Vl-propcase
A case property expression.
Vl-propcore
Basic, single expression in a sequence or property (perhaps with some probability distribution stuff.)
*vl-trivially-true-property-expr*
A vl-propexpr that is just true.
Vl-propexpr-fix
Fixing function for vl-propexpr structures.
Vl-propexpr-count
Measure for recurring over vl-propexpr structures.