From 17823579d39a7ea9082e69b646facfd08b1b9717 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Mon, 9 Mar 2020 11:14:38 -0400 Subject: [PATCH] Add proof for power_decoder2.DecodeA --- src/soc/decoder/formal/proof_decoder2.py | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/src/soc/decoder/formal/proof_decoder2.py b/src/soc/decoder/formal/proof_decoder2.py index e9e15cdd..651dcbf7 100644 --- a/src/soc/decoder/formal/proof_decoder2.py +++ b/src/soc/decoder/formal/proof_decoder2.py @@ -3,7 +3,8 @@ 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 +from soc.decoder.power_enums import (In1Sel, In2Sel, In3Sel, + InternalOp, SPR) from soc.decoder.power_decoder2 import (PowerDecode2, Decode2ToExecute1Type) import unittest @@ -28,8 +29,26 @@ class Driver(Elaboratable): return m def test_in1(self, m, pdecode2, pdecode): + 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) + 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) + 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 + 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) + 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) class Decoder2TestCase(FHDLTestCase): -- 2.30.2