I'll have to take your word for parts of this because I'm not familiar with this proof.
I'm not sure x86 decoding is oh-so-simple, because if you bring in memory the alignment is not guaranteed so you don't even know where the instruction starts let alone where it ends. An x86 instruction can theoretically have an unbounded number of prefixes, meaningful only after decoding something after that - maybe you can do it with a FSM but an enormous one.
All in all this doesn't sound like a master's project in the slightest, because remember I said design and verify not just build a never-used-again toy.
There have been probably hundreds of millions of dollars spent on this over the years, and they're basically stuck on the current width and multiple pipeline stages.
Just as I expected: finite-state machine used to decode. Now write a FSM-compiler (which is an undergrad-level project), to automatically parallelize the implementation.
The parallelization step is probably Master's level, but a very advanced undergrad student can probably accomplish it: since all the individual elements are undergrad projects (Kogge-stone applied to associative operators, finite-state machine compiler / regular expressions)
As a FSM, verification is simple. Just generate all x86 instructions (there are a finite number of them after all), and ensure your FSM properly goes through all of them.
That state machine looks ahead more than one symbol and has a lot of memory even if you consider it one big state.
You have to verify it decodes invalid instructions as a fault which means testing the entire search space.
Hypothetically you could use a bounded model check but you need to test roughly 10^36 combinations which is still thousands of years if you can do a 1000 billion billion a second. You need a formal proof of the operation too.
You can formally verify a finite state machine by simply testing all state-transitions.
You don't need to do an exhaustive check of the 2^8^15 all 15-byte combinations. You just check all state-transitions of the state machine.
Or to put it another way: you don't need to test all 2^8^15 byte combinations. You just need to check all invalid-instructions that have ONE invalid byte, to prove the attributes of the finite-state-machine.
I'm not sure x86 decoding is oh-so-simple, because if you bring in memory the alignment is not guaranteed so you don't even know where the instruction starts let alone where it ends. An x86 instruction can theoretically have an unbounded number of prefixes, meaningful only after decoding something after that - maybe you can do it with a FSM but an enormous one.
All in all this doesn't sound like a master's project in the slightest, because remember I said design and verify not just build a never-used-again toy.
There have been probably hundreds of millions of dollars spent on this over the years, and they're basically stuck on the current width and multiple pipeline stages.