I usually find these by looking at the RTL schematics. Note that some passes inside the tool are performed differently based on utilisation, and the bug often won't show up if you synthesise that module by itself. Combinatorial logic (after several stages of optimisation) has the wrong value. Pipeline register mysteriously vanishes on one bit out of a vector. This isn't really a bug, and is easy to find and work around. Let me introduce you to the wonderful world of Vivado. (That's my time, not solver time-I tend to keep the time required by the solver to a minimum if possible.) Depending on the complexity of the component, though, the entire proof can take days to a week or so of my time to complete. In general, though, I can get the first runs through the formal solver going within a couple of hours-a day at the most. Using a property file that I'd developed some time ago, describing the required interaction between the CPU and the fetch interface, together with a bus property file, I had the entire component up and running (again) within the weekend.Īs a comparison and contrast, when I had tried something similar with an instruction cache-only testing it in simulation alone, I found myself spending a couple of weeks in FPGA Hell after declaring that the cache was working and placing it onto an FPGA.
The first data cache I wrote took me about two weeks to both write and complete a full formal proof.Īs an example, I recently converted a fetch interface from requiring the bus width equal the instruction width to one allowing arbitrary larger bus widths. I haven't (yet) done an out of order processor, although I will say that verifying a cache gets really basic with formal methods, and I've now verified several cache implementations. My experience comes from both the ZipCPU (a basic pipelined CPU) and verifying a lot of bus components.