<awygle>
I'm still interested in your observations tho, ZipCPU
<promach>
I have not indicated any specific solver in te makefile though
ZipCPU|Laptop has joined #yosys
<ZipCPU>
Try using yices. To do that, add "-s yices" to your yosys-smtbmc command line.
<ZipCPU>
(Assuming you have yices installed ....)
<awygle>
Iirc isn't yices the default?
<awygle>
I certainly have to specify Z3 on every run
<ZipCPU>
awygle: Either way, 100k plus iterations isn't going to be easy with *any* solver.
<awygle>
Sure. I wonder how much spinning up a fat AWS instance would help...
<awygle>
In other words, what is the limiting factor in performance and how does it scale
<awygle>
I'll add that to the list of things to investigate I suppose
<ZipCPU>
Well, consider this ... everything that can toggle will be toggled in a formal solver.
<ZipCPU>
Hence, if you can limit your inputs to being well-behaved, that lowers a 2^n search space down to n.
<ZipCPU>
For example, when does the transmitter receive its request?
<ZipCPU>
If the transmitter is busy, will the module controlling it make requests on one clock, withdraw its request on another, and make an additional request on a following clock?
<ZipCPU>
Or will the controller be well behaved, making one request at one out of N time-instants, and then holding that request for the rest of time.
<awygle>
Oh I very much agree that shrinking the space to search is a bigger win than throwing compute at it. But there's a fundamental limit on the former and only practical limits on the latter.
<awygle>
So I'm curious
<awygle>
I would expect it to be compute bound and parallel, but I wouldn't be surprised to learn it was serial or that it was thrashing out to disk a lot.
<ZipCPU>
awygle: The big thing I'm struggling with in promach's design is the fractional baud clock divider. It divides the input clock by (roughly) 5000x. My problem is ... I just don't know how to simplify that for the solver.
<ZipCPU>
promach: The difficult part regarding the assertion on line 29 of that module is that it will take roughly 5000 clocks (10k sim timesteps) to prove.
<ZipCPU>
To do that, the formal solver will need to maintain 2^32 initial states, and only weed them down to 1-2 after 5000 clock ticks.
<ZipCPU>
No, I take that back, ... the 2^32 possible states will be whittled down to roughly 860k after 5k clock ticks, not 1-2.
<awygle>
I assume you are proving this module independently? Not as part of the larger system?
<awygle>
I wonder what the effect would be if you reversed the order of the if and the assert