From: Michael Nolan Date: Wed, 11 Mar 2020 14:17:26 +0000 (-0400) Subject: Add assertions that instruction fields are correct X-Git-Tag: div_pipeline~1719 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=53ccb189507e8b695f4d153c68f2557344a5f94e;p=soc.git 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 30ae65db..8c9644c1 100644 --- 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):