Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Sv
Vwsim
Fgl
Vl
Syntax
Loader
Preprocessor
Vl-loadconfig
Vl-loadstate
Lexer
Parser
Parse-expressions
Parse-udps
Parse-statements
Parse-property
Vl-parse-property-list-of-arguments
Vl-parse-sequence-match-item
Vl-parse-property-actual-arg
Vl-parse-scoped-or-hierarchical-identifier
Vl-parse-cycledelayrange
*vl-end-of-sequence-$*
Vl-parse-sequence-abbrev
Vl-parse-boolean-abbrev
Vl-parse-1+-expression-or-dists-separated-by-commas
Vl-parse-property-acceptop
Vl-parse-dist-item
Vl-parse-sequence-match-item-list
Vl-parse-property-spec
Vl-parse-impl-prop-expr-op
Vl-parse-expression-or-dist
Vl-parse-dist-list
Vl-alternating-propexpr/op-list-p
Vl-left-associate-alternating-propexpr/op-list
Vl-left-associate-delay-se-tail
Vl-delay-se-tail-p
Vl-parse-1+-named-property-list-of-arguments
Vl-parse-property-low-prec-unary
Vl-parse-within-sequence-expr-aux
Vl-parse-throughout-sequence-expr
Vl-parse-or-property-expr-aux
Vl-parse-intersect-sequence-expr-aux
Vl-parse-intersect-sequence-expr
Vl-parse-delay-sequence-expr
Vl-parse-assign-sequence-expr
Vl-parse-and-property-expr-aux
Vl-parse-1+-property-case-items
Vl-parse-within-sequence-expr
Vl-parse-or-property-expr
Vl-parse-instance-property-expr
Vl-parse-iff-property-expr
Vl-parse-delay-sequence-expr-tail
Vl-parse-and-property-expr
Vl-parse-until-property-expr
Vl-parse-strength-property-expr
Vl-parse-repeat-sequence-expr
Vl-parse-property-expr
Vl-parse-property-case-item
Vl-parse-not-property-expr
Vl-parse-impl-property-expr
Vl-parse-firstmatch-sequence-expr
Vl-genelements
Parse-paramdecls
Parse-blockitems
Parse-utils
Parse-insts
Parse-functions
Parse-assignments
Parse-clocking
Parse-strengths
Vl-parse-genvar-declaration
Vl-parse
Parse-netdecls
Parse-asserts
Vl-maybe-parse-lifetime
Parse-dpi-import-export
Parse-ports
Parse-timeunits
Seq
Parse-packages
Parse-eventctrl
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
Vl-parse-cycledelayrange
*vl-end-of-sequence-$*
Definition:
*vl-end-of-sequence-$*
(
defconst
*vl-end-of-sequence-$* (
make-vl-special
:key :vl-$))