I saw your latest work in formal verification in Fayalite, nice!
I intend to port to Fayalite some nMigen tests I made when I was learning formal verification.
For the queue proof, I don't think you really need to stop the counters at index_max, in lines 287 and 309.
Let the counters wrap around, and the proof should be good for infinite time. I feel it can be made to work, as long as the difference between them is asserted to be always between 0 and index_max.
Thanks!
I've been running into a bunch of issues in CI though, the CI server has been locking up so I need to manually reboot it, I'm thinking either its running out of memory or maybe the CPU is wearing out and/or overheating -- I bought it in 2016 and the motherboard is much older...I didn't see anything relevant in the system logs. I'm probably going to switch to using the Ryzen 3900x and 32GB of DDR4 I was previously using in my desktop, though I have to get it back from my dad since I was lending it to him (my parents were in the middle of moving so were effectively living in two places, but ended up not moving after all so he doesn't need two computers anymore)...
Nice! Pull requests welcome, though I think we should start putting code in a different repo specifically for our cpu design instead of fayalite -- some things aren't general enough to be useful for nearly all digital hardware.
the counters start at zero so asserting the difference is between 0 and index max doesn't quite work...also you'd need to make sure it was properly handling when the index counters wrap around which imo is a bit annoying.
I'm thinking that asserting it works for ~232 data transfers is good enough, especially since the queue doesn't really have the state that would be needed to only start doing something weird after that many cycles.
So, since it works, I think I'll just leave it and go on to working on the next thing that isn't yet implemented.