From ccfa31af5fd40dc0a59504fb39b9d8f60f3a119e Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Tue, 10 Mar 2020 11:07:05 -0400 Subject: [PATCH] Refactor DecodeA test --- src/soc/decoder/formal/proof_decoder2.py | 44 +++++++++++++----------- 1 file changed, 24 insertions(+), 20 deletions(-) diff --git a/src/soc/decoder/formal/proof_decoder2.py b/src/soc/decoder/formal/proof_decoder2.py index 651dcbf7..ccdeda8f 100644 --- a/src/soc/decoder/formal/proof_decoder2.py +++ b/src/soc/decoder/formal/proof_decoder2.py @@ -11,45 +11,49 @@ import unittest class Driver(Elaboratable): def __init__(self): - pass + self.m = None + self.comb = None + def elaborate(self, platform): - m = Module() - comb = m.d.comb + self.m = Module() + self.comb = self.m.d.comb instruction = Signal(32) - comb += instruction.eq(AnyConst(32)) + self.comb += instruction.eq(AnyConst(32)) pdecode = create_pdecode() - m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode) - comb += pdecode2.dec.opcode_in.eq(instruction) + self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode) + self.comb += pdecode2.dec.opcode_in.eq(instruction) - self.test_in1(m, pdecode2, pdecode) + self.test_in1(pdecode2, pdecode) - return m + return self.m - def test_in1(self, m, pdecode2, pdecode): + def test_in1(self, pdecode2, pdecode): + m = self.m + comb = self.comb ra = pdecode.RA[0:-1] with m.If(pdecode.op.in1_sel == In1Sel.RA): - m.d.comb += Assert(pdecode2.e.read_reg1.data == ra) - m.d.comb += Assert(pdecode2.e.read_reg1.ok == 1) + comb += Assert(pdecode2.e.read_reg1.data == ra) + comb += Assert(pdecode2.e.read_reg1.ok == 1) with m.If(pdecode.op.in1_sel == In1Sel.RA_OR_ZERO): with m.If(ra == 0): - m.d.comb += Assert(pdecode2.e.read_reg1.ok == 0) + comb += Assert(pdecode2.e.read_reg1.ok == 0) with m.Else(): - m.d.comb += Assert(pdecode2.e.read_reg1.data == ra) - m.d.comb += Assert(pdecode2.e.read_reg1.ok == 1) - op = pdecode.op.internal_op + comb += Assert(pdecode2.e.read_reg1.data == ra) + comb += Assert(pdecode2.e.read_reg1.ok == 1) + op = pdecode.op.internal_op with m.If((op == InternalOp.OP_BC) | (op == InternalOp.OP_BCREG)): with m.If(~pdecode.BO[2]): - m.d.comb += Assert(pdecode2.e.read_spr1.data == SPR.CTR) - m.d.comb += Assert(pdecode2.e.read_spr1.ok == 1) + comb += Assert(pdecode2.e.read_spr1.data == SPR.CTR) + comb += Assert(pdecode2.e.read_spr1.ok == 1) with m.If((op == InternalOp.OP_MFSPR) | (op == InternalOp.OP_MTSPR)): - m.d.comb += Assert(pdecode2.e.read_spr1.data == pdecode.SPR[0:-1]) - m.d.comb += Assert(pdecode2.e.read_spr1.ok == 1) - + comb += Assert(pdecode2.e.read_spr1.data == + pdecode.SPR[0:-1]) + comb += Assert(pdecode2.e.read_spr1.ok == 1) class Decoder2TestCase(FHDLTestCase): def test_decoder2(self): -- 2.30.2