Since the progress of the project is so early, I decided now is a good time to start to learn how to develop cores using formal verification.  I've so far "proven" my ROMA core's slave TileLink port to my satisfaction, and I'm going to move on to working with the SIA.

I have implemented the baud rate generator logic using formal verification.  So far I'm pleased with the results, but I have to admit, I still have a lot to learn.  Will try to keep you folks updated with my progress.

I'm pleased to say that the ROMA core is now operational enough to meet my needs.  This is not to suggest that it implements the complete and total TileLink interface.  On the contrary, it does not.  If you send a PUT or PUT_PARTIAL request to the ROMA core, you'll deadlock, because it just doesn't know what to do with those yet.  (It will eventually, just not at the moment.)  However, if you send it a GET request, you'll get back a 64-bit word containing what you're looking for after about 97 clock cycles.  Remember that the ROM it's attaching to is a serial flash ROM, accessed one bit at a time.

So, progress!!

As indicated above, the next steps are to implement the transmit-side of the first SIA core.

I do have a SIA core implemented from last year (which is both TX and RX capable), but I'll be starting from scratch and incrementally copying the design over.  This way, I can work towards a formally-verified design from the ground up.  The alternative, taking an existing design and adding FV properties to it, takes much, much longer to complete because all the moving parts conspire to falsify your assertions in unforeseen ways.  So, by the time I'm done, the finished SIA design will inherit almost everything from last year's prototype design.  The register layout will be different, however.