4 ms·

What is this project? Can anyone ELI5?

• addaon 6y ago
  A core is the part of a processor that actually runs instructions -- a processor consists of one or more cores, peripherals, etc. Software consists of a sequence of instructions ("add A and B") that, together, accomplish a goal. But even perfect software is only correct if the core that it runs on is correct. Historically, there have been a small number of high-profile correctness issues in various processor cores (e.g. Intel's Pentium FDIV bug), and almost every processor has a number of small correctness issues documented in errata -- or, not yet discovered. In designing and building a processor, correctness is important, and hard -- generally, much more time is spent testing and demonstrating correctness of a core than actually designing it. Formal verification aims to not just test and demonstrate correctness, but prove it. That is, under certain assumptions, one can prove that, for example, the actual transistors used to implement "add A and B", when connected in the intended way, have the same semantics ("do the same thing") as "add A and B". In the extreme case, formal methods can replace testing. In practice, they can replace some portion of testing; but those assumptions that they're built on can be a bit shaky. Formal methods can also be /hard/ -- it can take more time to prove something correct than to just test it thoroughly enough to convince everyone. But, when done right, it does lead to higher confidence overall.