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
m.submodules.dut = dut = MultiCompUnit(regspec, alu, CompALUOpSubset)
# TODO Test shadow / die
m.d.comb += [dut.shadown_i.eq(1), dut.go_die_i.eq(0)]
+ # Don't issue while busy
+ issue = Signal()
+ m.d.comb += dut.issue_i.eq(issue & ~dut.busy_o)
# Avoid toggling go_i when rel_o is low (rel / go protocol)
rd_go = Signal(dut.n_src)
m.d.comb += dut.cu.rd.go_i.eq(rd_go & dut.cu.rd.rel_o)
cnt = Signal(4, name="cnt_write_%d" % i)
m.d.sync += cnt.eq(cnt + do_write[i])
cnt_write.append(cnt)
+ do_alu_write = Signal()
+ m.d.comb += do_alu_write.eq(alu.p.i_valid & alu.p.o_ready)
+ cnt_alu_write = Signal(4)
+ m.d.sync += cnt_alu_write.eq(cnt_alu_write + do_alu_write)
+ do_alu_read = Signal()
+ m.d.comb += do_alu_read.eq(alu.n.o_valid & alu.n.i_ready)
+ cnt_alu_read = Signal(4)
+ m.d.sync += cnt_alu_read.eq(cnt_alu_read + do_alu_read)
+ cnt_masked_read = []
+ for i in range(dut.n_src):
+ cnt = Signal(4, name="cnt_masked_read_%d" % 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_read[0] == 1)
- & (cnt_read[1] == 1)
+ & (cnt_read[1] == 0)
& (cnt_write[0] == 1)
- & (cnt_write[1] == 1))
+ & (cnt_write[1] == 1)
+ & (cnt_alu_write == 1)
+ & (cnt_alu_read == 1)
+ & (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__":