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
Warnings
Primitives
Use-set
Syntax
Getting-started
Utilities
Loader
Transforms
Expression-sizing
Occform
Oprewrite
Expand-functions
Delayredux
Unparameterization
Caseelim
Split
Selresolve
Weirdint-elim
Vl-delta
Replicate-insts
Rangeresolve
Propagate
Clean-selects
Clean-params
Blankargs
Inline-mods
Expr-simp
Trunc
Always-top
Edgesynth
Vl-edgesynth-stmt-p
Vl-edgetable-p
Vl-always-edgesynth
Vl-edgesynth-merge-data-ifs
Vl-assignstmtlist->controls
Vl-assignstmtlist->lhses
Vl-assignstmtlist->rhses
Vl-edgesynth-flatten-data-ifs
Vl-edgesynth-pattern-match
Nedgeflop
Vl-edgesynth-make-data-inputs
Vl-edgesynth-make-clock-inputs
Vl-edgesynth-stmt-clklift
Vl-edgesynth-blockelim
Vl-edgesynth-stmt-blockelim
Vl-edgesynth-stmtlist-blockelim
Vl-alwayslist-edgesynth
Vl-edgesynth-create
Vl-edgesynth-classify-iftest
Vl-module-edgesynth
Vl-edgesynth-normalize-ifs
Vl-edgesynth-delays-okp
Vl-edgesynth-stmt-assigns
Vl-make-edgetable
Vl-edgesynth-sort-edges
Vl-modulelist-edgesynth
Vl-modulelist-edgesynth-aux
Vl-assignstmtlist-p
Vl-edgesynth-edgelist-p
Vl-assigncontrols-p
Vl-edgesynth-stmt-conditions
Vl-edgesynth-edge-p
Vl-design-edgesynth
Vl-edgesynth-get-delay
Vl-edgesynth-iftype-p
Edge-tables
Stmtrewrite
Cblock
Vl-always-convert-regports
Vl-always-convert-regs
Stmttemps
Edgesplit
Vl-always-check-reg
Vl-convert-regs
Latchsynth
Vl-always-check-regs
Vl-match-always-at-some-edges
Unelse
Vl-always-convert-reg
Vl-design-always-backend
Vl-stmt-guts
Vl-always-convert-regport
Vl-always-scary-regs
Eliminitial
Ifmerge
Vl-edge-control-p
Elimalways
Gatesplit
Gate-elim
Expression-optimization
Elim-supplies
Wildelim
Drop-blankports
Clean-warnings
Addinstnames
Custom-transform-hooks
Annotate
Latchcode
Elim-unused-vars
Problem-modules
Lint
Mlib
Server
Kit
Printer
Esim-vl
Well-formedness
Sv
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vl-edgesynth-blockelim
Vl-edgesynth-stmt-blockelim
Signature
(vl-edgesynth-stmt-blockelim x curr) → new-stmt
Arguments
x
— Statement we're rewriting, from the top down.
Guard
(
and
(
vl-stmt-p
x) (
vl-edgesynth-stmt-p
x))
.
curr
— Statement we've constructed so far, from any previous statements in the current begin/end block. Could be a NULL statement if we haven't seen any other statements yet.
Guard
(
and
(
vl-stmt-p
curr) (
vl-edgesynth-stmt-p
curr))
.
Returns
new-stmt
—
Type
(
vl-edgesynth-stmt-p
new-stmt)
, given the
guard
.