From c39e98213055bfcbebb0c55da65f2ba3edaa806d Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Fri, 2 Sep 2022 13:32:45 +0100 Subject: [PATCH] add fix of out_sel in power_decoder.py formal proof but there are others. basically the list of enums needs to be automatically listed and put into the matches --- src/openpower/decoder/formal/test_decoder.py | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/openpower/decoder/formal/test_decoder.py b/src/openpower/decoder/formal/test_decoder.py index f0053134..0236d93a 100644 --- a/src/openpower/decoder/formal/test_decoder.py +++ b/src/openpower/decoder/formal/test_decoder.py @@ -99,7 +99,7 @@ class Driver(Elaboratable): 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 + # The table has fields for XO and Rc, what do they match to? with self.m.Case(Form.B): pass with self.m.Case(Form.D): @@ -109,7 +109,8 @@ class Driver(Elaboratable): In2Sel.CONST_UI, In2Sel.CONST_SI, In2Sel.CONST_UI_HI, In2Sel.CONST_SI_HI)) self.comb += Assert(dec.op.out_sel.matches( - OutSel.NONE, OutSel.RT, OutSel.RA)) + OutSel.NONE, OutSel.RT, OutSel.RA, OutSel.SPR, + OutSel.RT_OR_ZERO, OutSel.FRT, OutSel.FRS)) with self.m.Case(Form.I): self.comb += Assert(dec.op.in2_sel.matches( In2Sel.CONST_LI)) @@ -122,8 +123,11 @@ class Driver(Elaboratable): class DecoderTestCase(FHDLTestCase): @unittest.expectedFailure # FIXME: proof failed: - # self.comb += Assert(dec.op.out_sel.matches( - # OutSel.NONE, OutSel.RT, OutSel.RA)) + # needs to have all the enum entries added, TODO there + # has to be an automated way to do that + # self.comb += Assert(dec.op.in2_sel.matches( + # In2Sel.CONST_UI, In2Sel.CONST_SI, In2Sel.CONST_UI_HI, + # In2Sel.CONST_SI_HI)) def test_decoder(self): module = Driver() self.assertFormal(module, mode="bmc", depth=4) -- 2.30.2