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
Address
Wire
Module
Lhs
Lhs.lisp
Lhs-vars-normorderedp
Lhs-norm
Lhatom-normorderedp
Lhs-normp
Svex-lhsrewrite-aux
Lhs-concat
Lhs-check-masks
Lhrange-combine
Svexarr-vars-aux
Assigns-check-masks
Svex->lhs-range
Svex-lhs-preproc-blkrev
Svarlist-boundedp-badguy
Driverlist-rest-after-strength
Aliases-normorderedp
Lhs-rsh
Lhs-cons
Svarlist-boundedp
Lhs-bitproj
Lhs-vars
Driver
Svex-override
Make-simple-lhs
Lhssvex-range-p
Lhs-override
Lhs-first-aux
Lhrange-combinable-dec
Lhrange-bitproj
Lhatom
Driverlist-values-of-strength
Lhs-rest-aux
Lhs-rest
Aliases-normorderedp-aux
Svexarr-vars
Lhsarr-to-svexarr
Svexarr-vars-witness-aux
Lhbit
Svex-lhsrewrite
Svar-boundedp
Lhs-decomp-aux
Svex->lhs-bound
Aliases-vars-aux
Svexarr
Svexarr-vars-witness
Svar-set-index
Lhsarr
Lhs-override-vars
Lhatom-eval-zero
Lhatom-bitproj
Lhrange-nextbit
Lhrange-combinable
Driverlist->svex
Svexlist-resolve
Lhs->svex-zero
Lhs-overridelist-vars
Lhs-overridelist-keys
Lhbit-eval
Driverlist-vars
Assigns-vars
Svex-int
Lhssvex-bounded-p
Lhslist-vars
Lhs-decomp
Lhatom-vars
Svar-map-vars
Lhssvex-unbounded-p
Lhspairs-vars
Lhs-width
Aliases-vars
Lhs-first
Svar-index
Assigns
Svar-indexedp
Lhspairs
Svex-overridelist
Lhslist
Lhs-overridelist
Driverlist
Svex-lhs-preproc
Svexarr-fix
Lhsarr-fix
Lhs-p
Lhs-fix
Lhrange
Lhs-eval-zx
Lhs-equiv
Lhs-eval
Lhs->svex
Path
Svar-add-namespace
Design
Modinst
Lhs-add-namespace
Modalist
Path-add-namespace
Modname->submodnames
Name
Constraintlist-addr-p
Svex-alist-addr-p
Svar-map-addr-p
Lhspairs-addr-p
Modname
Assigns-addr-p
Lhs-addr-p
Lhatom-addr-p
Modhier-list-measure
Attributes
Modhier-measure
Modhier-list-measure-aux
Modhier-loopfreelist-p
Modhier-loopfree-p
Svstmt
Sv-tutorial
Expressions
Symbolic-test-vector
Vl-to-svex
Fgl
Vwsim
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Lhs
Lhs.lisp
Subtopics
Lhs-vars-normorderedp
Lhs-norm
Lhatom-normorderedp
Lhs-normp
Svex-lhsrewrite-aux
Lhs-concat
Lhs-check-masks
Lhrange-combine
Svexarr-vars-aux
Assigns-check-masks
Svex->lhs-range
Svex-lhs-preproc-blkrev
Svarlist-boundedp-badguy
Driverlist-rest-after-strength
Aliases-normorderedp
Lhs-rsh
Lhs-cons
Svarlist-boundedp
(svarlist-boundedp x bound)
recognizes lists where every element satisfies
svar-boundedp
.
Lhs-bitproj
Lhs-vars
Driver
Svex-override
Make-simple-lhs
Lhssvex-range-p
Lhs-override
Lhs-first-aux
Lhrange-combinable-dec
Lhrange-bitproj
Lhatom
Driverlist-values-of-strength
Lhs-rest-aux
Lhs-rest
Aliases-normorderedp-aux
Svexarr-vars
Lhsarr-to-svexarr
Svexarr-vars-witness-aux
Lhbit
Svex-lhsrewrite
Svar-boundedp
Lhs-decomp-aux
Svex->lhs-bound
Aliases-vars-aux
Svexarr
Abstract stobj: logically this just represents a list of
|SV|::|SVEX-P|
s, but it is implemented as an array.
Svexarr-vars-witness
Svar-set-index
Lhsarr
Abstract stobj: logically this just represents a list of
|SV|::|LHS-P|
s, but it is implemented as an array.
Lhs-override-vars
Lhatom-eval-zero
Lhatom-bitproj
Lhrange-nextbit
Lhrange-combinable
Driverlist->svex
Svexlist-resolve
Lhs->svex-zero
Lhs-overridelist-vars
Lhs-overridelist-keys
Lhbit-eval
Driverlist-vars
Assigns-vars
Svex-int
Lhssvex-bounded-p
Lhslist-vars
Lhs-decomp
Lhatom-vars
Svar-map-vars
Lhssvex-unbounded-p
Lhspairs-vars
Lhs-width
Aliases-vars
Lhs-first
Svar-index
Assigns
An alist mapping
lhs-p
to
driver-p
.
Svar-indexedp
Lhspairs
An alist mapping
lhs-p
to
lhs-p
.
Svex-overridelist
A list of
svex-override-p
objects.
Lhslist
A list of
lhs-p
objects.
Lhs-overridelist
A list of
lhs-override-p
objects.
Driverlist
A list of
driver-p
objects.
Svex-lhs-preproc
Preprocesses an expression into one that only contains concat, rsh, and signx operators.
Svexarr-fix
Lhsarr-fix
