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
Software-verification
Kestrel-books
X86isa
Program-execution
Dynamic-instrumentation
Initialize-x86-state
Binary-file-load-fn
Read-channel-into-byte-list1
Setting-up-page-tables
Init-zero-page
Load-file-into-memory
Linux-load
Init-sys-view
Load-elf-sections
Chars-to-c-str
String-to-c-str
Pack-u64
Pack-u32
Concrete-simulation-examples
Fibonacci32-cosim
Fibonacci-cosim
Factorial-cosim
Nop-cosim
Datacopy-cosim
Gdt-entry
Sdm-instruction-set-summary
Tlb
Booting-linux
Introduction
Asmtest
X86isa-build-instructions
Publications
Contributors
Machine
Implemented-opcodes
To-do
Proof-utilities
Peripherals
Model-validation
Modelcalls
Concrete-simulation-examples
Fibonacci32-cosim
Fibonacci-cosim
Factorial-cosim
Nop-cosim
Datacopy-cosim
Utils
Debugging-code-proofs
Axe
Execloader
Math
Testing-utilities
Program-execution
X86isa
Concrete-simulation-examples
Subtopics
Fibonacci32-cosim
Test to check if a 32-bit fibonacci program behaves as expected
Fibonacci-cosim
Test to check if a fibonacci program behaves as expected
Factorial-cosim
Test to check if a factorial program behaves as expected
Nop-cosim
Test to see if the
Recommended multi-byte sequence of NOP Instruction
(Intel Vol. 2B, NOP Instruction-Set Reference) is supported by the
x86isa
model
Datacopy-cosim
Test to check if an array copy program works as expected