A question to those active in chip design industry: Are formal methods and formally proving a design more prevalent and normal in this industry compared to general software development?

Like for a Arm microcontroller design, do engineers thoroughly test and formally prove the correct functionality of every component? If that's the case, why silicon errata is a thing?

There are tools for formal verification of design input, and they are being used, but not for everything.

Why there are still errata for silicon

1. Writing a formal specification of your intended behavior is hard and the best verification tool doesn't help when your assertions don't encode the required or intended behavior. So even with 100% formal coverage, you would still get erratas. And some people don't write any formal verification, instead working with a simulation based approach (either hand-written test cases or random stimulus simulation) 2. Computation complexity of formal verification is exponential. At some point you simply can't formally prove the behavior of a design, because it just won't run on your server. 3. There's different levels of formal verification, not all of them are in the spec -> behavior path. For example, you could classify automated checks like logic equivalence between the synthesis netlist and RTL code as a formal verification. But that checks if the optimizer in the synthesis tool was correct, not that you wrote the correct RTL.

Compared to software formal methods have greater adoption. But there are a lot of things that fall under the “formal” umbrella.

The most common type that is used would probably be logical equivalence checking. Proving RTL and a netlist are equivalent is useful for catching synthesis bugs.

Or proving two netlists are equivalent after inserting test functions directly into a netlist, or some other netlist edit.

Property checking is what I use the most. You can check these during simulation which I wouldn’t call “formal” but you can also prove them using tools that use SAT solvers and whatnot to prove things mathematically.

As always, the tricky part of verification is writing the correct test or model. With formal we can use SystemVerilog assertions to write properties and sequences, but the difficulty in getting them right goes from trivial -> inscrutable very quickly.

It’s extreme easy to write assertions that pass and never realize your assertion was not doing what you thought and you weren’t proving what you meant to.

I haven’t used some of the more advanced tools so maybe they have ways to make this easier. But because of this I tend to just write assertions that are pretty easy to understand at a glance, and therefore closer to the trivial side of things.

If a peer has to solve a sudoku puzzle in their head to understand your work, then it’s unlikely the peer review will be worth anything. So I do what I can to make my work understandable at a glance (from a competent peer in the industry).

Of course making something simple can be quite challenging and often takes more time than leaving something complex and opaque.

I’ve never been involved in the foundry side of the work, and for ASICs, that is often half of the schedule.

It’s called design verification, formal proofs happen mostly at the EDA tool level and largely already automated. Design verification focus on functional correctness of the chip for its intended use case