# 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