Some things you just can't make up. Do you really want new, untested, unproven technology in your brand new IC? You do know that will add risk to your project, right?

Don't you just love it when a high priced, commercial EDA tool gives you an error and ... neither the error message, the man page, nor Google offer any help?

Formally verifying my AXIDMA can take a week or longer of solid CPU time. Today, I fired the proof off using the CVC5 solver. (cvc5 Solver) Other solvers attempting the proof include Z3, Yices2, and Boolector. Let's see which one finishes first.

Why formally verify a DMA? Consider this, running off the end of memory should generate a DMA error. One DMA passed all of its simulation tests, yet would only generate a memory overflow error under some stall conditions. Were those the ones simulated, or were they missed?

There seems to be a lot of misunderstanding regarding *formal* verification. Let me ask this question, then: which tool will find all the bugs?

Well, the first test was a failure. Power's been going out here regularly every day in the late afternoon. When the CPU is on high power, the UPS can't keep up and everything shuts down. All I know so far is that the proof will take longer than 5hrs independent of the solver.

See ... this is the problem I have with most of the commercial tools I have access to ... I have access to the tools, but not the courseware and ... I can't figure out where to start with their documentation. At least with open source tooling you can google any thing you need to

Second test failed when the power browned out after 7 hrs. I'm now browsing UPS battery power on Amazon ...

My Dad, a CrayOS developer, once tried to write a language he called "D". I'm not sure if it ever made it out of his office. It certainly never caught on.