From a1b4d5af90f265dee84db8641325d519d7ae0617 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Fri, 17 Jul 2020 18:44:16 +0100 Subject: [PATCH] use convenience vars in spr proof --- src/soc/fu/spr/formal/proof_main_stage.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/soc/fu/spr/formal/proof_main_stage.py b/src/soc/fu/spr/formal/proof_main_stage.py index 730ffdbd..cb98bf65 100644 --- a/src/soc/fu/spr/formal/proof_main_stage.py +++ b/src/soc/fu/spr/formal/proof_main_stage.py @@ -54,6 +54,8 @@ class Driver(Elaboratable): ca_in = dut.i.xer_ca[0] # CA carry in ca32_in = dut.i.xer_ca[1] # CA32 carry in 32 so_in = dut.i.xer_so # SO sticky overflow + ov_in = dut.i.xer_ov[0] # XER OV in + ov32_in = dut.i.xer_ov[1] # XER OV32 in o = dut.o.o # setup random inputs @@ -118,8 +120,8 @@ class Driver(Elaboratable): with m.Case(SPR.XER): bits = { 'SO': so_in, - 'OV': dut.i.xer_ov[0], - 'OV32': dut.i.xer_ov[1], + 'OV': ov_in, + 'OV32': ov32_in, 'CA': ca_in, 'CA32': ca32_in, } -- 2.30.2