From 5ceac486f4c0faa2a8307d10dc1c5b4b8e826259 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 18 Mar 2020 09:35:07 -0400 Subject: [PATCH] Add proof that all other opcodes decode to INVALID --- src/soc/decoder/formal/proof_decoder.py | 4 ++++ 1 file changed, 4 insertions(+) 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: -- 2.30.2