From 9c6ac6322596835af840457248e2d92878f6eb82 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Tue, 10 Mar 2020 11:22:44 -0400 Subject: [PATCH] Add cases for DecodeB and DecodeC --- src/soc/decoder/formal/proof_decoder2.py | 63 ++++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/src/soc/decoder/formal/proof_decoder2.py b/src/soc/decoder/formal/proof_decoder2.py index ccdeda8f..53848be7 100644 --- a/src/soc/decoder/formal/proof_decoder2.py +++ b/src/soc/decoder/formal/proof_decoder2.py @@ -27,6 +27,8 @@ class Driver(Elaboratable): self.comb += pdecode2.dec.opcode_in.eq(instruction) self.test_in1(pdecode2, pdecode) + self.test_in2() + self.test_in3() return self.m @@ -55,6 +57,67 @@ class Driver(Elaboratable): pdecode.SPR[0:-1]) comb += Assert(pdecode2.e.read_spr1.ok == 1) + def test_in2(self): + m = self.m + comb = self.comb + pdecode2 = m.submodules.pdecode2 + dec = pdecode2.dec + with m.If(dec.op.in2_sel == In2Sel.RB): + comb += Assert(pdecode2.e.read_reg2.ok == 1) + comb += Assert(pdecode2.e.read_reg2.data == + dec.RB[0:-1]) + with m.Elif(dec.op.in2_sel == In2Sel.NONE): + comb += Assert(pdecode2.e.imm_data.ok == 0) + comb += Assert(pdecode2.e.read_reg2.ok == 0) + with m.Elif(dec.op.in2_sel == In2Sel.SPR): + comb += Assert(pdecode2.e.imm_data.ok == 0) + comb += Assert(pdecode2.e.read_reg2.ok == 0) + comb += Assert(pdecode2.e.read_spr2.ok == 1) + with m.If(dec.FormXL.XO[9]): + comb += Assert(pdecode2.e.read_spr2.data == SPR.CTR) + with m.Else(): + comb += Assert(pdecode2.e.read_spr2.data == SPR.LR) + with m.Else(): + comb += Assert(pdecode2.e.imm_data.ok == 1) + with m.Switch(dec.op.in2_sel): + with m.Case(In2Sel.CONST_UI): + comb += Assert(pdecode2.e.imm_data.data == dec.UI[0:-1]) + with m.Case(In2Sel.CONST_SI): + comb += Assert(pdecode2.e.imm_data.data == dec.SI[0:-1]) + with m.Case(In2Sel.CONST_UI_HI): + comb += Assert(pdecode2.e.imm_data.data == + (dec.UI[0:-1] << 4)) + with m.Case(In2Sel.CONST_SI_HI): + comb += Assert(pdecode2.e.imm_data.data == + (dec.SI[0:-1] << 4)) + with m.Case(In2Sel.CONST_LI): + comb += Assert(pdecode2.e.imm_data.data == + (dec.LI[0:-1] << 2)) + with m.Case(In2Sel.CONST_BD): + comb += Assert(pdecode2.e.imm_data.data == + (dec.BD[0:-1] << 2)) + with m.Case(In2Sel.CONST_DS): + comb += Assert(pdecode2.e.imm_data.data == + (dec.DS[0:-1] << 2)) + with m.Case(In2Sel.CONST_M1): + comb += Assert(pdecode2.e.imm_data.data == ~0) + with m.Case(In2Sel.CONST_SH): + comb += Assert(pdecode2.e.imm_data.data == dec.sh[0:-1]) + with m.Case(In2Sel.CONST_SH32): + comb += Assert(pdecode2.e.imm_data.data == dec.SH32[0:-1]) + with m.Default(): + comb += Assert(0) + + def test_in3(self): + m = self.m + comb = self.comb + pdecode2 = m.submodules.pdecode2 + with m.If(pdecode2.dec.op.in3_sel == In3Sel.RS): + comb += Assert(pdecode2.e.read_reg3.ok == 1) + comb += Assert(pdecode2.e.read_reg3.data == + pdecode2.dec.RS[0:-1]) + + class Decoder2TestCase(FHDLTestCase): def test_decoder2(self): module = Driver() -- 2.30.2