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
Vwsim
Fgl
Vl
Syntax
Loader
Warnings
Getting-started
Utilities
Printer
Kit
Vl-lint
Vl-lintconfig-p
Condcheck
Lint-warning-suppression
Lucid
Lvaluecheck
Vl-interfacelist-alwaysstyle
Truncation-warnings
Vl-modulelist-alwaysstyle
Skip-detection
Vl-lint-report
Vl-lintresult
Vl::vl-design-sv-use-set
Oddexpr-check
Vl-interfacelist-oddexpr-check
Vl-packagelist-oddexpr-check
Vl-modulelist-oddexpr-check
Vl-warn-odd-binary-expression-main
*vl-odd-binops-table*
Vl-oddinfo
Vl-oddinfo-fix
Make-vl-oddinfo
Vl-oddinfo-equiv
Vl-oddinfo-p
Change-vl-oddinfo
Vl-oddinfo->swidth
Vl-oddinfo->subexpr
Vl-oddinfo->simple
Vl-oddinfo->cwidth
Vl-oddinfo->complex
Vl-oddinfo->type
Vl-warn-odd-binary-expression
Vl-expr-probable-selfsize
Vl-interface-oddexpr-check
Vl-package-oddexpr-check
Vl-odd-binop-class
Vl-module-oddexpr-check
Vl-expr-oddexpr-check
Vl-oddinfo-details
Vl-ctxexprlist-oddexpr-check
Vl-oddinfolist-details
Vl-design-oddexpr-check
Vl-ctxexprlist-oddexpr-check-nrev
Vl-oddinfolist
Leftright-check
Duplicate-detect
Selfassigns
*vl-lint-help*
Arith-compare-check
Dupeinst-check
Qmarksize-check
Lint-whole-file-suppression
Run-vl-lint-main
Logicassign
Run-vl-lint
Vl-print-certain-warnings
Duperhs-check
Vl-lint-top
Sd-filter-problems
Vl-modulelist-add-svbad-warnings
Vl-module-add-svbad-warnings
Check-case
Vl-lint-extra-actions
Drop-lint-stubs
Vl-lint-print-warnings
Drop-user-submodules
Check-namespace
Vl-lintconfig-loadconfig
Vl-lint-design->svex-modalist-wrapper
Vl-delete-sd-problems-for-modnames-aux
Vl-collect-new-names-from-orignames
Vl-lint-print-all-warnings
Vl-design-remove-unnecessary-modules
Vl-delete-sd-problems-for-modnames
Vl-always-check-style
Vl-vardecllist-svbad-warnings
Vl-vardecl-svbad-warnings
Vl-reportcard-remove-suppressed
Vl-reportcard-keep-suppressed
Vl-alwayslist-check-style
Vl-remove-nameless-descriptions
Vl-lint-apply-quiet
Vl-warninglist-remove-suppressed
Vl-warninglist-keep-suppressed
Vl-print-eliminated-descs
Vl-module-alwaysstyle
Vl-jp-reportcard-aux
Vl-interface-alwaysstyle
Vl-design-alwaysstyle
Vl-jp-description-locations
Vl-jp-reportcard
Vl-pp-stringlist-lines
Vl-jp-design-locations
Vl-datatype-svbad-p
Unpacked-range-check
Sd-problem-major-p
Vl-alwaysstyle
Vl-server
Vl-gather
Vl-zip
Vl-main
Split-plusargs
Vl-shell
Vl-json
Mlib
Transforms
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Oddexpr-check
Vl-oddinfo
This is a product type introduced by
defprod
.
Fields
type —
symbolp
subexpr —
vl-expr
The whole subexpression
simple —
vl-expr
The simple side of the subexpression
complex —
vl-expr
The complex side of the subexpression
swidth —
maybe-natp
Simple side width
cwidth —
maybe-natp
Complex side width
Subtopics
Vl-oddinfo-fix
Fixing function for
vl-oddinfo
structures.
Make-vl-oddinfo
Basic constructor macro for
vl-oddinfo
structures.
Vl-oddinfo-equiv
Basic equivalence relation for
vl-oddinfo
structures.
Vl-oddinfo-p
Recognizer for
vl-oddinfo
structures.
Change-vl-oddinfo
Modifying constructor for
vl-oddinfo
structures.
Vl-oddinfo->swidth
Get the
swidth
field from a
vl-oddinfo
.
Vl-oddinfo->subexpr
Get the
subexpr
field from a
vl-oddinfo
.
Vl-oddinfo->simple
Get the
simple
field from a
vl-oddinfo
.
Vl-oddinfo->cwidth
Get the
cwidth
field from a
vl-oddinfo
.
Vl-oddinfo->complex
Get the
complex
field from a
vl-oddinfo
.
Vl-oddinfo->type
Get the
type
field from a
vl-oddinfo
.