From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Sat, 1 Aug 2020 09:49:08 +0000 (+0100)
Subject: expand out for-loop setting up input record subset
X-Git-Tag: semi_working_ecp5~475
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=77e41a06502264d4c7e8642090c3df0b5edc3747;p=soc.git

expand out for-loop setting up input record subset
this to help in formal proof shiftrot analysis
---

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)