From 2f033d1bb26662cd1dea19a0d723bf021de3e17e Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Wed, 20 May 2020 17:54:34 +0100 Subject: [PATCH] formal proof rename on XER flags --- src/soc/fu/alu/formal/proof_output_stage.py | 10 +++++----- src/soc/fu/logical/formal/proof_main_stage.py | 7 ++++--- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/soc/fu/alu/formal/proof_output_stage.py b/src/soc/fu/alu/formal/proof_output_stage.py index 9e33f148..ff838d91 100644 --- a/src/soc/fu/alu/formal/proof_output_stage.py +++ b/src/soc/fu/alu/formal/proof_output_stage.py @@ -43,12 +43,12 @@ class Driver(Elaboratable): cr0 = Signal(4) so = Signal() comb += [dut.i.o.eq(o), - dut.i.carry_out.eq(carry_out), - dut.i.so.eq(so), - dut.i.carry_out32.eq(carry_out32), + dut.i.xer_ca[0].eq(carry_out), + dut.i.xer_so.eq(so), + dut.i.xer_ca[1].eq(carry_out32), dut.i.cr0.eq(cr0), - dut.i.ov.eq(ov), - dut.i.ov32.eq(ov32), + dut.i.xer_ov[0].eq(ov), + dut.i.xer_ov[1].eq(ov32), o.eq(AnyConst(64)), carry_out.eq(AnyConst(1)), carry_out32.eq(AnyConst(1)), diff --git a/src/soc/fu/logical/formal/proof_main_stage.py b/src/soc/fu/logical/formal/proof_main_stage.py index 7db2c40a..456ff815 100644 --- a/src/soc/fu/logical/formal/proof_main_stage.py +++ b/src/soc/fu/logical/formal/proof_main_stage.py @@ -51,14 +51,15 @@ class Driver(Elaboratable): # convenience variables a = dut.i.a b = dut.i.b - carry_in = dut.i.carry_in - so_in = dut.i.so + carry_in = dut.i.xer_ca[0] + carry_in32 = dut.i.xer_ca[1] + so_in = dut.i.xer_so o = dut.o.o # setup random inputs comb += [a.eq(AnyConst(64)), b.eq(AnyConst(64)), - carry_in.eq(AnyConst(1)), + carry_in.eq(AnyConst(0b11)), so_in.eq(AnyConst(1))] comb += dut.i.ctx.op.eq(rec) -- 2.30.2