Add proof that all other opcodes decode to INVALID

[soc.git] / src / soc / decoder / formal / proof_decoder.py

diff --git a/src/soc/decoder/formal/proof_decoder.py b/src/soc/decoder/formal/proof_decoder.py
index a7b013b02ea1c70ed0989736dbf505326934f59a..a77b0e8681a7aee88bce37a97745422b9cdc3b59 100644 (file)
--- a/src/soc/decoder/formal/proof_decoder.py
+++ b/src/soc/decoder/formal/proof_decoder.py
@@ -57,6 +57,10 @@ class Driver(Elaboratable):
                         continue
                     with self.m.Case(opcode):
                         self.comb += self.assert_dec1_signals(dec1, row)
+                with self.m.Default():
+                    self.comb += Assert(dec.op.internal_op ==
+                                        InternalOp.OP_ILLEGAL)
+                                        
 
     def handle_subdecoders(self, dec1, decoders):
         for dec in decoders.subdecoders: