Refactor DecodeA test
authorMichael Nolan <mtnolan2640@gmail.com>
Tue, 10 Mar 2020 15:07:05 +0000 (11:07 -0400)
committerMichael Nolan <mtnolan2640@gmail.com>
Tue, 10 Mar 2020 15:07:05 +0000 (11:07 -0400)
src/soc/decoder/formal/proof_decoder2.py

index 651dcbf7673ba1d9330cc76d9cc5ef2a5520f703..ccdeda8f9bfcfdf957aa26796d9a6967082a71ab 100644 (file)
@@ -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):