[EMAIL PROTECTED] wrote:
Before we discount math folk...I *did* think of a way to go a long way towards
a *proof* of the correctness of an emulator, at least relative to another
emulator. :)
Every ARM emulator accepts 32 bit instructions. 32 bits is "only" 4 billion.
I just need to compare the state of RAM, registers and CPU before and after a
32 bit instruction for a measly 4 billion of them!!! Maybe it would finish
overnight and so I could wake up with proof in hand!
Of course I'd have to do this for various initial states of CPU, RAM and
registers since hardware isn't stateless like HTML.
The keyword for what you are talking about is called "formal
verification." It's not easy.
Even verifying that something without state is correct is hard. Take,
for example, a 64bit x 64-bit multiplier. Simple energy considerations
automatically rule out combinatoric testing.
I recommend the book "Algorithms and Data Structures in VLSI Design" by
Meinel and Theobald. It's focus is on how to use Binary Decision
Diagrams (BDD's) to do logic verification in the presence of the
combinatoric explosion presented by most VLSI systems.
And, as an aside, just so you know, one of the few programming languages
to be formally verified is the Scheme48 system.
-a
--
[email protected]
http://www.kernel-panic.org/cgi-bin/mailman/listinfo/kplug-list
