Add assertions that instruction fields are correct

diff --git a/src/soc/decoder/formal/proof_decoder2.py b/src/soc/decoder/formal/proof_decoder2.py
index 30ae65db7102503e4df59fd113b0c56ef49d527a..8c9644c13d8206a5e6eb3f1fc787aaf8c3f47c4e 100644 (file)
--- a/src/soc/decoder/formal/proof_decoder2.py
+++ b/src/soc/decoder/formal/proof_decoder2.py
@@ -1,10 +1,10 @@
-from nmigen import Module, Signal, Elaboratable
+from nmigen import Module, Signal, Elaboratable, Cat
 from nmigen.asserts import Assert, AnyConst
 from nmigen.test.utils import FHDLTestCase
 
 from soc.decoder.power_decoder import create_pdecode, PowerOp
 from soc.decoder.power_enums import (In1Sel, In2Sel, In3Sel,
-                                     OutSel, RC,
+                                     OutSel, RC, Form,
                                      InternalOp, SPR)
 from soc.decoder.power_decoder2 import (PowerDecode2,
                                         Decode2ToExecute1Type)
@@ -14,21 +14,23 @@ class Driver(Elaboratable):
     def __init__(self):
         self.m = None
         self.comb = None
+        self.instruction = None
 
     def elaborate(self, platform):
         self.m = Module()
         self.comb = self.m.d.comb
-        instruction = Signal(32)
+        self.instruction = Signal(32)
 
-        self.comb += instruction.eq(AnyConst(32))
+        self.comb += self.instruction.eq(AnyConst(32))
 
         pdecode = create_pdecode()
 
         self.m.submodules.pdecode2 = pdecode2 = PowerDecode2(pdecode)
-        self.comb += pdecode2.dec.opcode_in.eq(instruction)
+        self.comb += pdecode2.dec.opcode_in.eq(self.instruction)
 
         self.test_in1(pdecode2, pdecode)
         self.test_in2()
+        self.test_in2_fields()
         self.test_in3()
         self.test_out()
         self.test_rc()
@@ -39,7 +41,7 @@ class Driver(Elaboratable):
     def test_in1(self, pdecode2, pdecode):
         m = self.m
         comb = self.comb
-        ra = pdecode.RA[0:-1]
+        ra = self.instr_bits(11, 15)
         with m.If(pdecode.op.in1_sel == In1Sel.RA):
             comb += Assert(pdecode2.e.read_reg1.data == ra)
             comb += Assert(pdecode2.e.read_reg1.ok == 1)
@@ -52,13 +54,13 @@ class Driver(Elaboratable):
                 op = pdecode.op.internal_op
         with m.If((op == InternalOp.OP_BC) |
                   (op == InternalOp.OP_BCREG)):
-            with m.If(~pdecode.BO[2]):
+            with m.If(~self.instr_bits(8)):
                 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)):
             comb += Assert(pdecode2.e.read_spr1.data ==
-                           pdecode.SPR[0:-1])
+                           self.instr_bits(11, 20))
             comb += Assert(pdecode2.e.read_spr1.ok == 1)
 
     def test_in2(self):
@@ -112,6 +114,21 @@ class Driver(Elaboratable):
                 with m.Default():
                     comb += Assert(0)
 
+    def test_in2_fields(self):
+        m = self.m
+        comb = self.comb
+        dec = m.submodules.pdecode2.dec
+
+        comb += Assert(dec.RB[0:-1] == self.instr_bits(16, 20))
+        comb += Assert(dec.UI[0:-1] == self.instr_bits(16, 31))
+        comb += Assert(dec.SI[0:-1] == self.instr_bits(16, 31))
+        comb += Assert(dec.LI[0:-1] == self.instr_bits(6, 29))
+        comb += Assert(dec.BD[0:-1] == self.instr_bits(16, 29))
+        comb += Assert(dec.DS[0:-1] == self.instr_bits(16, 29))
+        comb += Assert(dec.sh[0:-1] == Cat(self.instr_bits(30),
+                                           self.instr_bits(16, 20)))
+        comb += Assert(dec.SH32[0:-1] == self.instr_bits(16, 20))
+
     def test_in3(self):
         m = self.m
         comb = self.comb
@@ -119,7 +136,7 @@ class Driver(Elaboratable):
         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])
+                           self.instr_bits(6,10))
 
     def test_out(self):
         m = self.m
@@ -138,9 +155,10 @@ class Driver(Elaboratable):
             comb += Assert(pdecode2.e.write_reg.ok == 1)
             data = pdecode2.e.write_reg.data
             with m.If(sel == OutSel.RT):
-                comb += Assert(data == dec.RT[0:-1])
+                comb += Assert(data == self.instr_bits(6, 10))
             with m.If(sel == OutSel.RA):
-                comb += Assert(data == dec.RA[0:-1])
+                comb += Assert(data ==
+                               self.instr_bits(11, 15))
 
     def test_rc(self):
         m = self.m
@@ -154,9 +172,11 @@ class Driver(Elaboratable):
         with m.If(sel == RC.ONE):
             comb += Assert(pdecode2.e.rc.data == 1)
         with m.If(sel == RC.RC):
-            comb += Assert(pdecode2.e.rc.data == dec.Rc[0:-1])
+            comb += Assert(pdecode2.e.rc.data ==
+                           dec.Rc[0:-1])
             comb += Assert(pdecode2.e.oe.ok == 1)
-            comb += Assert(pdecode2.e.oe.data == dec.OE[0:-1])
+            comb += Assert(pdecode2.e.oe.data ==
+                           dec.OE[0:-1])
 
     def test_single_bits(self):
         m = self.m
@@ -171,13 +191,18 @@ class Driver(Elaboratable):
         comb += Assert(e.is_32bit == dec.op.is_32b)
         comb += Assert(e.is_signed == dec.op.sgn)
         with m.If(dec.op.lk):
-            comb += Assert(e.lk == dec.LK[0:-1])
+            comb += Assert(e.lk == self.instr_bits(31))
         comb += Assert(e.byte_reverse == dec.op.br)
         comb += Assert(e.sign_extend == dec.op.sgn_ext)
         comb += Assert(e.update == dec.op.upd)
         comb += Assert(e.input_cr == dec.op.cr_in)
         comb += Assert(e.output_cr == dec.op.cr_out)
 
+    def instr_bits(self, start, end=None):
+        if not end:
+            end = start
+        return self.instruction[::-1][start:end+1]
+
 
 class Decoder2TestCase(FHDLTestCase):
     def test_decoder2(self):