Previously I wrote about setting up Yosys and Rosette to build your own Formal Verification backend. This was severly limited in scope as it only allowed you to deal with small combinational circuits. This can be extended to small sequential circuits.

Increases in design complexity of any digital circuit necessitates increased efforts spent on verification. This is resulting in verification of a design being shifted earlier and earlier in modern IC design. The problem of tackling the verification of a digial system is difficult. A subset of this effort would be spent verifying isolated functional blocks.