Hi! This post is the first in a series introducing formal verification of hardware circuits in Verilog (and similar hardware description languages). While there are a couple of good resources for formal, especially zipcpu.com, the literature is surprisingly sparse, especially including end to end examples.
In this series, I want to develop an intuition for formal verification from first principles, working up all the way to formally verifying a reasonably complex IP (perhaps a simple processor core) with examples. Lets get started!