From 6d8c3b05b64966aacd3393c02e8c2444cd035798 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Wed, 27 May 2020 15:28:30 +0100 Subject: [PATCH] check reg output Data.ok in shift_rot formal proof --- .../fu/shift_rot/formal/proof_main_stage.py | 24 +++++++++++++++---- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/src/soc/fu/shift_rot/formal/proof_main_stage.py b/src/soc/fu/shift_rot/formal/proof_main_stage.py index 6f03f1a6..968eecdd 100644 --- a/src/soc/fu/shift_rot/formal/proof_main_stage.py +++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py @@ -44,7 +44,7 @@ class Driver(Elaboratable): carry_in = dut.i.xer_ca[0] carry_in32 = dut.i.xer_ca[1] carry_out = dut.o.xer_ca - o = dut.o.o + o = dut.o.o.data # setup random inputs comb += [a.eq(AnyConst(64)), @@ -67,8 +67,13 @@ class Driver(Elaboratable): comb += a_signed.eq(a) comb += a_signed_32.eq(a[0:32]) + # must check Data.ok + o_ok = Signal() + comb += o_ok.eq(1) + # main assertion of arithmetic operations with m.Switch(rec.insn_type): + with m.Case(InternalOp.OP_SHL): comb += Assume(ra == 0) with m.If(rec.is_32bit): @@ -76,6 +81,7 @@ class Driver(Elaboratable): comb += Assert(o[32:64] == 0) with m.Else(): comb += Assert(o == ((a << b[0:7]) & ((1 << 64)-1))) + with m.Case(InternalOp.OP_SHR): comb += Assume(ra == 0) with m.If(~rec.is_signed): @@ -90,10 +96,18 @@ class Driver(Elaboratable): comb += Assert(o[32:64] == Repl(a[31], 32)) with m.Else(): comb += Assert(o == (a_signed >> b[0:7])) - #TODO - #with m.Case(InternalOp.OP_RLC): - #with m.Case(InternalOp.OP_RLCR): - #with m.Case(InternalOp.OP_RLCL): + #TODO + with m.Case(InternalOp.OP_RLC): + pass + with m.Case(InternalOp.OP_RLCR): + pass + with m.Case(InternalOp.OP_RLCL): + pass + with m.Default(): + comb += o_ok.eq(0) + + # check that data ok was only enabled when op actioned + comb += Assert(dut.o.o.ok == o_ok) return m -- 2.30.2