From 77e41a06502264d4c7e8642090c3df0b5edc3747 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Sat, 1 Aug 2020 10:49:08 +0100 Subject: [PATCH] expand out for-loop setting up input record subset this to help in formal proof shiftrot analysis --- .../fu/shift_rot/formal/proof_main_stage.py | 23 ++++++++++++++++--- 1 file changed, 20 insertions(+), 3 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 fa970012..f66cd709 100644 --- a/src/soc/fu/shift_rot/formal/proof_main_stage.py +++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py @@ -34,9 +34,26 @@ class Driver(Elaboratable): comb = m.d.comb rec = CompSROpSubset() - # Setup random inputs for dut.op - for p in rec.ports(): - comb += p.eq(AnyConst(p.width)) + # Setup random inputs for dut.op. do them explicitly so that + # we can see which ones cause failures in the debug report + #for p in rec.ports(): + # comb += p.eq(AnyConst(p.width)) + comb += rec.insn_type.eq(AnyConst(rec.insn_type.width)) + comb += rec.fn_unit.eq(AnyConst(rec.fn_unit.width)) + comb += rec.imm_data.imm.eq(AnyConst(rec.imm_data.imm.width)) + comb += rec.imm_data.imm_ok.eq(AnyConst(rec.imm_data.imm_ok.width)) + comb += rec.rc.rc.eq(AnyConst(rec.rc.rc.width)) + comb += rec.rc.rc_ok.eq(AnyConst(rec.rc.rc_ok.width)) + comb += rec.oe.oe.eq(AnyConst(rec.oe.oe.width)) + comb += rec.oe.oe_ok.eq(AnyConst(rec.oe.oe_ok.width)) + comb += rec.write_cr0.eq(AnyConst(rec.write_cr0.width)) + comb += rec.input_carry.eq(AnyConst(rec.input_carry.width)) + comb += rec.output_carry.eq(AnyConst(rec.output_carry.width)) + comb += rec.input_cr.eq(AnyConst(rec.input_cr.width)) + comb += rec.is_32bit.eq(AnyConst(rec.is_32bit.width)) + comb += rec.is_signed.eq(AnyConst(rec.is_signed.width)) + comb += rec.insn.eq(AnyConst(rec.insn.width)) + pspec = ShiftRotPipeSpec(id_wid=2) m.submodules.dut = dut = ShiftRotMainStage(pspec) -- 2.30.2