Wishbone SVA Evaluation

This issue is used to document planning and progress for the Wishbone SVA evaluation.

In brief, we want to take [existing Wishbone SVA](https://zipcpu.com/zipcpu/2017/11/07/wb-formal.html) and find divergence between our protocol definition and the SVA (agnostic of any specific RTL implementation). Hopefully, the divergence will be of the sort where our Protocol is more precise to the actual Wishbone English-language specification.

These are the key steps:
- We need to check that our current BMC automaton in #281 are correct, and merge it in.
- We need to be able to switch between driver and *monitor* automata, or at least codegen transition systems for monitor
- We need to write a wishbone pipeline protocol since that's what the SVA we have is for. The SVA also has some extra conventions not technically in the Wishbone spec (the Wishbone spec is underspecified in places), so I don't know exactly what to do about that.
- our automata probably need to reach a fixed point for efficient monitoring (we can't have the exponential growth required by the current naive BMC automaton). This is because we can't really get larger than 6-8 trace length right now, and it's a bit slow, so I feel like this is gonna be trouble for doing BMC well. If there is not a finite cycle length after the fork in pipelined wishbone, then we need to add bound annotations to loops.
- We need to be able to take the SVA and generate Btor2 from it via Yosys. I'm looking into [SymbiYosys documentation](https://yosyshq.readthedocs.io/_/downloads/sby/en/latest/pdf/) to do this and [this](https://yosyshq.readthedocs.io/projects/yosys/en/0.41/cmd/read_verilog.html) etc.
- We then need to combine the transition systems for the SVA and the monitor together. I guess the new "bad state" would be the state where only one but not the other reaches its own bad state. I really have no clue if this will work, particularly given we have no functional model. I guess we'll see?
- Bounded model check the combined transition system.

Here are the risk of each step:
- I think switching between driver/monitor automata and the fixed-point monitoring are low risk. We pretty much know this is at least possible; it might be a little hard to engineer, but it can be done.
- We need to make sure we can actually represent pipelined wishbone in Protocols. I think it can, but it will require work if we can't (or if we need to add support for repeat and for/in finally). Worst case, we need a brand new construct. This is pretty high risk.
- Edit 6/30: I don't think there is a way for us to handle pipelined wishbone properly. It would require some sort of ordering data structure for FIFOs where we can send multiple requests (I guess for/in can do this), but then when the kth "ACK" is given it needs to be *matched* with the *kth* request we sent. We have no way of doing this right now. The SVA given has an `F_MAX_REQUESTS` parameter which I will set to one to make this evaluation tractable without adding new language features (which would be quite complicated).
- I added some extra logic regarding aborts and errors and stalls that our previous implementation did not handle.
- We need to make sure the SVA can actually be lowered to Btor2 by Yosys. If it can't, we may need to find another strategy to do this. This is pretty high risk. (Edit 6/29: This works!)

I am going to start with the high risk stuff.

Start with the BMC automaton work in #281, then read the linked SymbiYosys and Yosys read_verilog documentation to assess the SVA-to-Btor2 path. Completion involves checking the automaton, supporting monitor code generation, comparing Wishbone behavior, combining transition systems, and bounded-model-checking the result.

Written by the indexing model from the issue text.