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.