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
Fgl-rewrite-rules
Fgl-function-mode
Fgl-object
Fgl-solving
Fgl-handling-if-then-elses
Fgl-getting-bits-from-objects
Fgl-primitive-and-meta-rules
Fgl-interpreter-overview
Fgl-counterexamples
Fgl-correctness-of-binding-free-variables
Fgl-debugging
Fgl-testbenches
Def-fgl-boolean-constraint
Fgl-stack
Fgl-rewrite-tracing
Def-fgl-param-thm
Def-fgl-thm
Fgl-fast-alist-support
Fgl-array-support
Advanced-equivalence-checking-with-fgl
Solve-lane-by-lane-masked
Solve-lane-by-lane-masked+
Top-level-equal
Replace-equal-with-top-level-equal-rec
Solve-lane-by-lane
Lookup-previous-stack-frame-binding
Ipasir-sat-limit100
Fgl-internals
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Fgl
Advanced-equivalence-checking-with-fgl
Some tools for equivalence checking with FGL.
Subtopics
Solve-lane-by-lane-masked
Equality check that works around hard SAT/fraiging problems caused by writemasking.
Solve-lane-by-lane-masked+
Equality check that works around hard SAT/fraiging problems caused by writemasking, solving each case separately.
Top-level-equal
An alias for EQUAL. Useful if you want to prove an equality in FGL using a particular strategy.
Replace-equal-with-top-level-equal-rec
Solve-lane-by-lane
Equality check that, in FGL, splits an equivalence of SIMD packed integers into lane-by-lane equivalence checks.
Lookup-previous-stack-frame-binding
Ipasir-sat-limit100