signed, ResetSignal)
from nmigen.asserts import (Assert, AnyConst, Assume, Cover, Initial,
Rose, Fell, Stable, Past)
-from nmigen.test.utils import FHDLTestCase
+from nmutil.formaltest import FHDLTestCase
+from nmutil.gtkw import write_gtkw
from nmigen.cli import rtlil
import unittest
+import os
from soc.fu.compunits.compunits import FunctionUnitBaseSingle
from soc.experiment.alu_hier import DummyALU
from soc.experiment.compalu_multi import MultiCompUnit
-from soc.fu.alu.alu_input_record import CompALUOpSubset
+from soc.fu.cr.cr_input_record import CompCROpSubset
class Driver(Elaboratable):
m = Module()
comb = m.d.comb
sync = m.d.sync
+ inspec = [('INT', 'a', '0:15'),
+ ('INT', 'b', '0:15'),
+ ('INT', 'c', '0:15')]
+ outspec = [('INT', 'o', '0:15')]
+
+ regspec = (inspec, outspec)
alu = DummyALU(16)
- m.submodules.dut = dut = MultiCompUnit(16, alu, CompALUOpSubset)
+ m.submodules.dut = dut = MultiCompUnit(regspec, alu, CompCROpSubset)
issue = dut.issue_i
busy = dut.busy_o
- go_rd = dut.rd.go
- rd_rel = dut.rd.rel
+ go_rd = dut.rd.go_i
+ rd_rel = dut.rd.rel_o
- go_wr = dut.wr.go
- wr_rel = dut.wr.rel
+ go_wr = dut.wr.go_i
+ wr_rel = dut.wr.rel_o
go_die = dut.go_die_i
shadow_n = dut.shadown_i
comb += Assume(issue == 0)
comb += Assume(go_rd == 0)
comb += Assume(rst == 1)
+
with m.Else():
comb += Assume(rst == 0)
# cycle. Read requests may go out immediately after issue
# goes low
-
# The read_request should not happen while the unit is not busy
with m.If(~busy):
comb += Assert(rd_rel == 0)
with m.If(wr_rel == 0):
comb += Assume(go_wr == 0)
-
# Property 8: When go_write is asserted, two things
# happen. 1 - the data in the temp register is placed
# combinatorially onto the output. And 2 - the req_l latch
# then the alu data should be output
with m.If(Past(wr_rel) & Past(go_wr)):
# the alu data is output
- comb += Assert((dut.data_o == alu_temp) | (dut.data_o == dut.alu.o))
+ comb += Assert((dut.data_o == alu_temp)
+ | (dut.data_o == dut.alu.o))
# wr_rel is dropped
comb += Assert(wr_rel == 0)
# busy is dropped.
with m.If(~Past(go_die)):
comb += Assert(busy == 0)
-
# It is REQUIRED that issue be held valid only for one cycle
with m.If(Past(issue)):
comb += Assume(issue == 0)
class FUTestCase(FHDLTestCase):
def test_formal(self):
+ style = {
+ 'in': {'color': 'orange'},
+ 'out': {'color': 'yellow'},
+ }
+ traces = [
+ 'clk',
+ ('operation port', {'color': 'red'}, [
+ 'cu_issue_i', 'cu_busy_o',
+ {'comment': 'shadow / go_die'},
+ 'cu_shadown_i', 'cu_go_die_i']),
+ ('operand 1 port', 'in', [
+ ('cu_rd__rel_o[2:0]', {'bit': 2}),
+ ('cu_rd__go_i[2:0]', {'bit': 2}),
+ 'src1_i[15:0]']),
+ ('operand 2 port', 'in', [
+ ('cu_rd__rel_o[2:0]', {'bit': 1}),
+ ('cu_rd__go_i[2:0]', {'bit': 1}),
+ 'src2_i[15:0]']),
+ ('operand 3 port', 'in', [
+ ('cu_rd__rel_o[2:0]', {'bit': 0}),
+ ('cu_rd__go_i[2:0]', {'bit': 0}),
+ 'src1_i[15:0]']),
+ ('result port', 'out', [
+ 'cu_wr__rel_o', 'cu_wr__go_i', 'dest1_o[15:0]']),
+ ('alu', {'submodule': 'alu'}, [
+ ('prev port', 'in', [
+ 'oper_i_None__insn_type', 'i1[15:0]',
+ 'valid_i', 'ready_o']),
+ ('next port', 'out', [
+ 'alu_o[15:0]', 'valid_o', 'ready_i'])])]
+
+ write_gtkw('test_fu_formal_bmc.gtkw',
+ os.path.dirname(__file__) +
+ '/proof_fu_formal/engine_0/trace.vcd',
+ traces, style,
+ clk_period=10e-9,
+ time_resolution_unit="ns",
+ module='top.dut')
+
module = Driver()
self.assertFormal(module, mode="bmc", depth=10)
self.assertFormal(module, mode="cover", depth=10)
+
def test_ilang(self):
- dut = MultiCompUnit(16, DummyALU(16), CompALUOpSubset)
+ inspec = [('INT', 'a', '0:15'),
+ ('INT', 'b', '0:15'),
+ ('INT', 'c', '0:15')]
+ outspec = [('INT', 'o', '0:15')]
+
+ regspec = (inspec, outspec)
+ dut = MultiCompUnit(regspec, DummyALU(16), CompCROpSubset)
vl = rtlil.convert(dut, ports=dut.ports())
with open("multicompunit.il", "w") as f:
f.write(vl)