From 0727449813c38994029b1e0694c058ab7b714677 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Mon, 8 Jun 2020 13:33:31 +0100 Subject: [PATCH] move datamerger proof into standard directory location (formal/), update comments --- src/soc/experiment/{ => formal}/proof_datamerger.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) rename src/soc/experiment/{ => formal}/proof_datamerger.py (94%) diff --git a/src/soc/experiment/proof_datamerger.py b/src/soc/experiment/formal/proof_datamerger.py similarity index 94% rename from src/soc/experiment/proof_datamerger.py rename to src/soc/experiment/formal/proof_datamerger.py index dd44449e..722c6915 100644 --- a/src/soc/experiment/proof_datamerger.py +++ b/src/soc/experiment/formal/proof_datamerger.py @@ -1,4 +1,4 @@ -# Proof of correctness for partitioned equal signal combiner +# Proof of correctness for DataMerger # Copyright (C) 2020 Michael Nolan # Copyright (C) 2020 Tobias Platen @@ -36,8 +36,8 @@ class Driver(Elaboratable): for j in range(dut.array_size): allzero = (dut.addr_array_i[j] == 0) & allzero - # assert that the output is zero when the datamerger is idle with m.If(allzero): + # assert that the output is zero when the datamerger is idle comb += Assert(dut.data_o == 0) with m.Else(): comb += Assume(dut.data_o != 0) # at least one output bit is set -- 2.30.2