I was inspired by this blog post to take the same aproach for NESTang's SDRAM controller, and as an intermediate step I converted the big FSM to 3 FSMs (init, refresh, read-write) and formally verified each module.
Somewhere inbetween I saw no need to implement Dan's ultra-uC anymore, but I thought it would be nice to keep the FSMs and verification. 100% your choice @nand2mario to merge the PR or just let it die :)
I was inspired by this blog post to take the same aproach for NESTang's SDRAM controller, and as an intermediate step I converted the big FSM to 3 FSMs (init, refresh, read-write) and formally verified each module.
Somewhere inbetween I saw no need to implement Dan's ultra-uC anymore, but I thought it would be nice to keep the FSMs and verification. 100% your choice @nand2mario to merge the PR or just let it die :)