I'm just trying to get a feel for things here. I'm a hardware design engineer by trade. I'm familiar with the concepts of formal verification with regard to designing hardware. I'm less familiar with formal verification in the context of developing software.
The funny thing is that formal verification was original conceived with software development in mind, but the problem was too unbounded and it was never really practical.
So, my question is, "How many of today's software developers -- both high-level application developers and more firmware-inclined embedded systems developers -- do you think are aware of the concept of formal verification (a) in general and (b) with regard to software?"
Any feedback will be very much appreciated as always :-)
Hi Max. I think most are aware of the concept, but I suspect that almost nobody actually does it. There's an editorial in the July issue of the Communications of the ACM by Moshe Vardi on this very issue(DOI:10.1145/3469113). He points out that formal verification isn't done for many reasons, but also compares formal verification with Model Checking, which is easier and cheaper. The main obstacle to formal verification is its cost, according to Vardi. For hardware designs, where the cost of fixing a defect is very high, it makes sense, whereas for most software, the cost of fixing a defect isn't as high. At least that's the perception. Hardware designs are also not as free-form as most large software projects, and formal verification is tractable.
John
Hi John -- Thanks so much for your response -- do you mind if I quote your response in a column I'm writing?
No, I don't mind! :)
Cool Beans -- How would you like to be referred to (name, position, link to LinkedIn)?
Hi Max.
I'm John Ford, Principal Engineer at Steward Observatory, University of Arizona.
Make sure to keep your eyes open for my column on EEJournal.com thsi coming Thursday :-)
No, we were not able to use it, because we needed a 5 megabit per second uart and didn't have enough clock cycles to mux the inputs in. We ended up with enough space in the FPGA to do individual UARTs once I got the design completed.
I've got it in my bag of tricks if it's ever needed!
That’s too bad you weren’t able to use it, but glad that you were successful
