From 5fe221fda62b538a9f49784e28bd9e7b69923b8d Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Sun, 9 Oct 2022 18:01:36 -0300 Subject: [PATCH] Count zero_a and imm_data.ok as masked read transactions --- src/soc/experiment/formal/proof_compalu_multi.py | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/soc/experiment/formal/proof_compalu_multi.py b/src/soc/experiment/formal/proof_compalu_multi.py index d81f35e1..8f75b7b0 100644 --- a/src/soc/experiment/formal/proof_compalu_multi.py +++ b/src/soc/experiment/formal/proof_compalu_multi.py @@ -35,7 +35,7 @@ https://bugs.libre-soc.org/show_bug.cgi?id=197 import unittest from nmigen import Signal, Module -from nmigen.hdl.ast import Cover +from nmigen.hdl.ast import Cover, Const from nmutil.formaltest import FHDLTestCase from nmutil.singlepipe import ControlBase @@ -141,7 +141,13 @@ class CompALUMultiTestCase(FHDLTestCase): cnt_masked_read = [] for i in range(dut.n_src): cnt = Signal(4, name="cnt_masked_read_%d" % i) - m.d.sync += cnt.eq(cnt + (do_issue & dut.rdmaskn[i])) + if i == 0: + extra = dut.oper_i.zero_a + elif i == 1: + extra = dut.oper_i.imm_data.ok + else: + extra = Const(0, 1) + m.d.sync += cnt.eq(cnt + (do_issue & (dut.rdmaskn[i] | extra))) cnt_masked_read.append(cnt) # Ask the formal engine to give an example -- 2.30.2