From 80b7cd2e16253d6bc5de08c2352096490360ed31 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Wed, 11 Mar 2020 09:12:52 -0400 Subject: [PATCH] Add tests for DecodeOut and DecodeRC --- src/soc/decoder/formal/proof_decoder2.py | 39 ++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/src/soc/decoder/formal/proof_decoder2.py b/src/soc/decoder/formal/proof_decoder2.py index 53848be7..311cf01f 100644 --- a/src/soc/decoder/formal/proof_decoder2.py +++ b/src/soc/decoder/formal/proof_decoder2.py @@ -4,6 +4,7 @@ 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, InternalOp, SPR) from soc.decoder.power_decoder2 import (PowerDecode2, Decode2ToExecute1Type) @@ -29,6 +30,8 @@ class Driver(Elaboratable): self.test_in1(pdecode2, pdecode) self.test_in2() self.test_in3() + self.test_out() + self.test_rc() return self.m @@ -117,6 +120,42 @@ class Driver(Elaboratable): comb += Assert(pdecode2.e.read_reg3.data == pdecode2.dec.RS[0:-1]) + def test_out(self): + m = self.m + comb = self.comb + pdecode2 = m.submodules.pdecode2 + sel = pdecode2.dec.op.out_sel + dec = pdecode2.dec + with m.If(sel == OutSel.SPR): + comb += Assert(pdecode2.e.write_spr.ok == 1) + comb += Assert(pdecode2.e.write_reg.ok == 0) + with m.Elif(sel == OutSel.NONE): + comb += Assert(pdecode2.e.write_spr.ok == 0) + comb += Assert(pdecode2.e.write_reg.ok == 0) + with m.Else(): + comb += Assert(pdecode2.e.write_spr.ok == 0) + 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]) + with m.If(sel == OutSel.RA): + comb += Assert(data == dec.RA[0:-1]) + + def test_rc(self): + m = self.m + comb = self.comb + pdecode2 = m.submodules.pdecode2 + sel = pdecode2.dec.op.rc_sel + dec = pdecode2.dec + comb += Assert(pdecode2.e.rc.ok == 1) + with m.If(sel == RC.NONE): + comb += Assert(pdecode2.e.rc.data == 0) + 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]) + + class Decoder2TestCase(FHDLTestCase): def test_decoder2(self): -- 2.30.2