The https://zipcpu.com/zipcpu/2017/11/07/wb-formal.html ZipCPU formal wishbone is for pipelined wishbone, not for classic (which seems to be what our read/write protocols in examples/wishbone is for and also not the burst mode wishbone. So I think if we want to compare to this SVA, we will need to come up with a pipelined wishbone protocol (if we can). Seems like the wishbone test version does something that looks like pipelining, but it doesnt look right for me because it still waits for the ack before forking.
Since in pipelined mode we will need to fork before the while loop waiting for the ack, it means that we will not be able to find a steady state without placing a bound on the pipeline depth. this might require a new bound annotation on while loops.
The https://zipcpu.com/zipcpu/2017/11/07/wb-formal.html ZipCPU formal wishbone is for pipelined wishbone, not for classic (which seems to be what our read/write protocols in
examples/wishboneis for and also not the burst mode wishbone. So I think if we want to compare to this SVA, we will need to come up with a pipelined wishbone protocol (if we can). Seems like the wishbone test version does something that looks like pipelining, but it doesnt look right for me because it still waits for the ack before forking.Since in pipelined mode we will need to fork before the while loop waiting for the ack, it means that we will not be able to find a steady state without placing a bound on the pipeline depth. this might require a new
boundannotation on while loops.