		Search-engine friendly clone of the ACL2 documentation.

Sv-tutorial

Basic tutorial: how to use the svex package to do datapath verification.

The subtopics are listed in the intended order of the tutorial, which first covers verification of a simple 16-bit combinational ALU module, then a counter module to illustrate how to deal with state over time, and finally a multiplier implementation to show how to structurally decompose your proofs.

Note: A much higher level of detail is present in the comments of this book than in the xdoc tutorial. The xdoc tutorial is intended to give a high-level idea of how to do it; to actually replicate it, you will likely want to look at the sources.

To begin the ALU example, start at translating-verilog-to-svex.

Subtopics

Stvs-and-testing: Defining a simulation pattern (STV) and using it to run tests.
Decomposition-proofs: Proof by decomposing and re-composing a hardware model
Proofs-with-stvs: How to do proofs about hardware models using STVs and FGL.
Translating-verilog-to-svex: How to parse Verilog files and translate them into an svex design