Wishbone SVA Evaluation

[Nikil-Shyamsunder]

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

In brief, we want to take existing Wishbone SVA 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 BMC Automaton #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 to do this and this 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.

[ekiwi]

• I don't think there is a way for us to handle pipelined wishbone properly.

Could it be handled if we fix the pipeline delay? I.e. the response always comes back within one cycle?
If that work, then can we also deal with stalls?

[Nikil-Shyamsunder]

Ah, I think fixed pipeline delay would work! I suppose in this situation we would assert the ACK signal high after the pipeline delay number of cycles, and assert the data port is the expected value (if it's a read). I will need to think about handling stalls further, but I don't see why it wouldn't work; we would hold all the ports until STALL is low, then fork() and DontCare all the signals (except for CYC).