Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Sv
Svex-stvs
Svex-decomposition-methodology
Sv-versus-esim
Svex-decomp
Svex-compose-dfs
Svex-compilation
Moddb
Svmods
Svstmt
Sv-tutorial
Expressions
Symbolic-test-vector
Vl-to-svex
Vl-to-sv
Vl-design->sv-design
Vl-simpconfig
Vl-hierarchy-sv-translation
Vl-expr-svex-translation
Sv::vl-expr.lisp
Vl-scopecontext-to-addr
Vl-binaryop-to-svex
Vl-expr-to-svex-maybe-typed
Vl-datatype-syscall-to-svex
Vl-operandinfo-to-svex-preproc
Vl-structmemberlist->types
Vl-seltrace-to-svex-select
Vl-portdecllist->types
Vl-operandinfo-to-svex-select
Vl-plusminus-partselect->svex
Vl-arrayrange->rel-lsb-and-width
Vl-unaryop-to-svex
Vl-funcall-args-to-ordered
Vl-expr-to-svex-lhs
Vl-operandinfo-to-svex
Vl-array-assignpat-keyval-resolve
Vl-err->vfatal
Vl-datatypelist-usertype-resolve
Vl-upscope-to-svex-upscope
Vl-err->fatal
Vl-streaming-concat-trunc/extend
Vl-operandinfo-base-svar
Vl-index-shift-amount
Vttree->constraints
Vl-slicesize-resolve
Vl-function-map-find-matching-aux
Vl-funname-lookup
Vl-datatype-size-warn
Svex-repeat-aux
Vl-$test$plusargs-to-svex
Svex-extend
Vl-structmemberlist-shift-bits
Vl-datatype-slot-width/range
Vl-datatype-index-shift-amount
Vl-datatype-field-shift-amount
4vec-extend
Vl-function-pair-inputs-with-actuals
Vl-expr-to-svex-untyped
Vl-function-map-check-matching
Vl-datatype-syscall-remove-dims
Svex-concat-list-aux
Vttree-add-constraints
Vttree-add-warnings
Vl-check-struct-assignpat-keys
Vl-check-array-assignpat-keys
Sv::constraintlist-subst-memo
Vl-svex-keyval-index-lookup
Vl-function-map-find-matching
Vl-convert-dollarsign-to-expr
Vttree->constraints-acc
Vl-seltrace-type
Vl-seltrace-to-path
Vl-keyval-member-lookup
Svex-repeat
Vttree->warnings-acc
Vl-trunc/extend-type-err
Constraintlist-add-ctx
Vl-hidtrace-add-to-path
Svex-multiconcat
Vttree-join
Vl-value-to-string-aux
Vl-seltrace-add-to-path
Vl-value-to-4vec
Vl-expr-to-svex-selfdet
Vl-svex-keyval-default-lookup
Vl-$test$plusargs-p
Vl-value-to-svex
Vl-value-in-range
Vl-keyval-default-lookup
Sv::svexlist-args-extract-constants
Vl-string->bits
Vl-size-to-unsigned-logic
Vl-hidtrace-to-path
Svex-concat-list
Vttree->warnings
Vl-seltrace-unres-count
Vl-datatype-index-is-bitselect
Vl-bitlist->4vec
Vl-svex-keyvallist-vars
Vl-hidstep->svex-index
Vl-selstep->svex-name
Vl-datatypelist-resolved-p
Vl-datatype-$unpacked_dimensions
Vl-datatype-$dimensions
Vl-bitlist->offset
Vl-bitlist->onset
Vl-streamexprlist-has-with
Vl-hidstep-resolved-p
Vl-expr-needs-type-context
Vl-streamexprlist->exprs
Vl-integer-to-string
Vl-hidtrace-resolved-p
Vl-selstep-resolved-p
Vl-select-resolved-p
Vl-svex-keyvallist
Vl-svex-keyvallist-p
Vl-svex-keyvallist-fix
Vl-svex-keyvallist-equiv
Vl-datatypelist
Svex-x
Vttree
Vl-design->svex-modalist
Vl-svstmt
Vl-to-sv-main
Vl-simplify-sv
Vl-user-paramsettings->unparam-names
Vl-user-paramsettings->modnames
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Sv::vl-expr.lisp
Vl-svex-keyvallist
An alist mapping
vl-patternkey-p
to
sv::svex-p
.
This is an ordinary
fty::defalist
.
Subtopics
Vl-svex-keyvallist-p
Recognizer for
vl-svex-keyvallist
.
Vl-svex-keyvallist-fix
(vl-svex-keyvallist-fix x)
is an
fty
alist fixing function that follows the fix-keys strategy.
Vl-svex-keyvallist-equiv
Basic equivalence relation for
vl-svex-keyvallist
structures.