Comment by laydn

9 years ago

I've done formal verification on several units of a microprocessor, and I can assure you, formal verification on individual FUs is very, very ambitious (think impossible) for a modern microprocessor.

For example, you can not possibly formally verify the fetcher unit on its own, because the state space that you need to cover for several cycles for all the module inputs and outputs is beyond the capability of any formal verification tool.

Typically, you run formal verification on sub-blocks of sub-blocks of FUs.

For this particular bug, it looks like multiple functional units are involved, so it might have been missed by formal verification.

5 comments

laydn

wyager 9 years ago

> because the state space that you need to cover for several cycles for all the module inputs and outputs is beyond the capability of any formal verification tool.

Then use a proof methodology that doesn't require exhaustive enumeration. This objection is actually fairly alarming to me; perhaps there is a larger disconnect between industrial formal techniques for hardware and software than I thought. Strings also occupy a "large state space", but this obviously doesn't prevent us from doing formal verification on functions over strings.

Confusion 9 years ago
Then use a proof methodology that doesn't require exhaustive enumeration.
You may as well have said "then you use a magical tool that doesn't exist".
Strings also occupy a "large state space", but this obviously doesn't prevent us from doing formal verification on functions over strings.
What is your reason to think this is 'obviously' the case?
- wyager 9 years ago
  
  > You may as well have said "then you use a magical tool that doesn't exist".
  Ok, so what this tells me is that you're not aware of what modern verification techniques look like.
  There's not really any one resource I can point you to, but take a look at these links. I've used these or similar technologies personally, but there are others I haven't used.
  https://en.m.wikipedia.org/wiki/Intuitionistic_type_theory
  https://en.m.wikipedia.org/wiki/Homotopy_type_theory
  https://leanprover.github.io/about/
  http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
  > What is your reason to think this is 'obviously' the case?
  Because I've done this, and anyone who claims to be familiar with formal methods should be at least passingly familiar with all the things I mentioned.
  Even if you aren't, if you've ever heard of SAT (a fairly universal CS concept) you should at least be familiar with the idea that non-exhaustive proofs are a thing.
  
  1 reply →

jlouis 9 years ago

I've had great success (in software) with randomized/probability based testing. You don't walk the full state space but generate subsets randomly to walk.

If done naively, it doesn't work because you are unlikely to hit the problematic bug. So you have to be clever: do not generate inputs uniformly! Generate those inputs which are really really nasty all the time. If you find a problem, then gradually simplify the case until you have reduced the complexity to something which can be understood.

With some experience for where former bugs tend to live, I've been able to remove lots of bugs from my software in edge cases via this method. (See "QuickCheck").