From: Michael Nolan <mtnolan2640@gmail.com>
Date: Wed, 18 Mar 2020 13:35:07 +0000 (-0400)
Subject: Add proof that all other opcodes decode to INVALID
X-Git-Tag: div_pipeline~1682
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ceac486f4c0faa2a8307d10dc1c5b4b8e826259;p=soc.git

Add proof that all other opcodes decode to INVALID
---

diff --git a/src/soc/decoder/formal/proof_decoder.py b/src/soc/decoder/formal/proof_decoder.py
index a7b013b0..a77b0e86 100644
--- 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: