# SPDX-License-Identifier: LGPLv3+
# Copyright (C) 2022 Cesar Strauss <cestrauss@gmail.com>
-# Sponsored by NLnet and NGI POINTER under EU Grants 871528 and 957073
+# Sponsored by NLnet under EU Grant and 957073
# Part of the Libre-SOC Project.
"""
import unittest
from nmigen import Signal, Module
-from nmigen.hdl.ast import Cover
+from nmigen.hdl.ast import Cover, Const, Assume, Assert
from nmutil.formaltest import FHDLTestCase
from nmutil.singlepipe import ControlBase
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)
+ # If the ALU is idle, do not assert valid
+ with m.If(cnt_alu_read == cnt_alu_write):
+ m.d.comb += Assume(~alu.n.o_valid)
+
+ # Invariant check
+ # For every instruction issued, at any point in time,
+ # each operand was either:
+ # 1) Already read
+ # 2) Not read yet, but the read is pending (rel_o high)
+ # 3) Masked
+ for i in range(dut.n_src):
+ sum_read = Signal(4)
+ m.d.comb += sum_read.eq(
+ cnt_read[i] + cnt_masked_read[i] + dut.cu.rd.rel_o[i])
+ m.d.comb += Assert(sum_read == cnt_issue)
# Ask the formal engine to give an example
m.d.comb += Cover((cnt_issue == 2)
& (cnt_masked_read[0] == 1)
& (cnt_masked_read[1] == 1))
self.assertFormal(m, mode="cover", depth=10)
+ # Check assertions
+ self.assertFormal(m, mode="bmc", depth=10)
if __name__ == "__main__":