@carrot0Today I got enough courage to try formal verification. Wrote proof for a byte-addressable RAM controller and it passed! (along with identifying some race condition bugs)
This uses Symbiyosys with boolector as the smtbmc solver (k-type temporal induction).
github.com/HomebrewSiliconClub/Processor/blob/master/rtl/soc/bram_ctl.v#L106
@anthonykung0Can't decide whether to go with blue or pink...
