Allow the formal engine to perform a same-cycle result in the ALU

[soc.git] / src / soc / decoder / formal / proof_decoder.py

diff --git a/src/soc/decoder/formal/proof_decoder.py b/src/soc/decoder/formal/proof_decoder.py
index 94e0c913eeb5d2a8071e393df0b042d1bf43f7a8..ce19a4265d6422b9fe5f09bafaa6bfde294422e6 100644 (file)
--- a/src/soc/decoder/formal/proof_decoder.py
+++ b/src/soc/decoder/formal/proof_decoder.py
@@ -1,13 +1,13 @@
 from nmigen import Module, Signal, Elaboratable, Cat
 from nmigen.asserts import Assert, AnyConst, Assume
-from nmigen.test.utils import FHDLTestCase
+from nmutil.formaltest import FHDLTestCase
 
-from soc.decoder.power_decoder import create_pdecode, PowerOp
-from soc.decoder.power_enums import (In1Sel, In2Sel, In3Sel,
+from openpower.decoder.power_decoder import create_pdecode, PowerOp
+from openpower.decoder.power_enums import (In1Sel, In2Sel, In3Sel,
                                      OutSel, RC, Form, Function,
                                      LdstLen, CryIn,
-                                     InternalOp, SPR, get_csv)
-from soc.decoder.power_decoder2 import (PowerDecode2,
+                                     MicrOp, SPR, get_csv)
+from openpower.decoder.power_decoder2 import (PowerDecode2,
                                         Decode2ToExecute1Type)
 import unittest
 import pdb
@@ -29,7 +29,8 @@ class Driver(Elaboratable):
 
         self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
         dec1 = pdecode2.dec
-        self.comb += pdecode2.dec.opcode_in.eq(self.instruction)
+        self.comb += pdecode2.dec.bigendian.eq(1) # TODO: bigendian=0
+        self.comb += pdecode2.dec.raw_opcode_in.eq(self.instruction)
 
         # ignore special decoding of nop
         self.comb += Assume(self.instruction != 0x60000000)
@@ -57,6 +58,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 ==
+                                        MicrOp.OP_ILLEGAL)
+                                        
 
     def handle_subdecoders(self, dec1, decoders):
         for dec in decoders.subdecoders:
@@ -70,7 +75,7 @@ class Driver(Elaboratable):
     def assert_dec1_signals(self, dec, row):
         op = dec.op
         return [Assert(op.function_unit == Function[row['unit']]),
-                Assert(op.internal_op == InternalOp[row['internal op']]),
+                Assert(op.internal_op == MicrOp[row['internal op']]),
                 Assert(op.in1_sel == In1Sel[row['in1']]),
                 Assert(op.in2_sel == In2Sel[row['in2']]),
                 Assert(op.in3_sel == In3Sel[row['in3']]),
@@ -81,15 +86,19 @@ class Driver(Elaboratable):
                 Assert(op.form == Form[row['form']]),
                 ]
 
+    # This is to assert that the decoder conforms to the table listed
+    # in PowerISA public spec v3.0B, Section 1.6, page 12
     def assert_form(self, dec, dec2):
         with self.m.Switch(dec.op.form):
             with self.m.Case(Form.A):
-                self.comb += Assert(dec2.e.write_reg.data ==
-                                    self.instr_bits(6, 10))
-                self.comb += Assert(dec2.e.read_reg1.data ==
-                                    self.instr_bits(11, 15))
-                self.comb += Assert(dec2.e.read_reg2.data ==
-                                    self.instr_bits(16, 20))
+                self.comb += Assert(dec.op.in1_sel.matches(
+                    In1Sel.NONE, In1Sel.RA, In1Sel.RA_OR_ZERO))
+                self.comb += Assert(dec.op.in2_sel.matches(
+                    In2Sel.RB, In2Sel.NONE))
+                self.comb += Assert(dec.op.in3_sel.matches(
+                    In3Sel.RS, In3Sel.NONE))
+                self.comb += Assert(dec.op.out_sel.matches(
+                    OutSel.NONE, OutSel.RT))
                 # The table has fields for XO and Rc, but idk what they correspond to
             with self.m.Case(Form.B):
                 pass
@@ -101,10 +110,10 @@ class Driver(Elaboratable):
                     In2Sel.CONST_SI_HI))
                 self.comb += Assert(dec.op.out_sel.matches(
                     OutSel.NONE, OutSel.RT, OutSel.RA))
-                        
-                
-                
-        
+            with self.m.Case(Form.I):
+                self.comb += Assert(dec.op.in2_sel.matches(
+                    In2Sel.CONST_LI))
+
     def instr_bits(self, start, end=None):
         if not end:
             end = start