+# This is the proof for the computation unit/Function Unit/ALU
+# manager. Description here:
+# https://libre-soc.org/3d_gpu/architecture/compunit/
+
+# This attempts to prove most of the bullet points on that page
+
from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
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):
def __init__(self):
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 = dut.shadown_i
+ shadow_n = dut.shadown_i
rst = ResetSignal()
has_issued = Signal(reset=0)
-
-
with m.If(init):
comb += Assume(has_issued == 0)
comb += Assume(issue == 0)
comb += Assume(go_rd == 0)
comb += Assume(rst == 1)
+
with m.Else():
comb += Assume(rst == 0)
- # detect when issue has been raised and remember it
- with m.If(issue):
- sync += has_issued.eq(1)
- comb += Cover(has_issued)
+ # Property 1: When issue is first raised, a busy signal is
+ # sent out. The operand can be latched in at this point
+ # (rd_rel and go_rd are allowed to be high)
- # Property 1: after an issue, busy should be raised
+ # Busy should rise after issue.
with m.If(Past(issue)):
- comb += Assert(busy)
-
- # Property 2: After a wr_rel and go_wr, busy should be lowered
- with m.If(Past(wr_rel) & Past(go_wr)):
- # Shadow interferes with this and I'm not sure what is
- # correct
- with m.If(~Past(shadow)):
- comb += Assert(busy == 0)
- with m.Elif(Past(busy) == 1):
- comb += Assert(busy == 1)
-
- # Property 3: Rd_rel should never be asserted before issue
-
- # If issue has never been raised, then rd_rel should never
- # be raised
- with m.If(rd_rel != 0):
- comb += Assert(has_issued)
-
- # Property 4: when rd_rel is asserted, it should stay
- # that way until a go_rd
- with m.If((Past(go_rd) == 0) & ~Past(go_die)):
- comb += Assert(~Fell(rd_rel))
-
- # Property 5: when a bit in rd_rel is asserted, and
- # the corresponding bit in go_rd is asserted, then that
- # bit of rd_rel should be deasserted
- for i in range(2):
- with m.If(Past(go_rd)[i] & (Past(rd_rel) != 0)):
- comb += Assert(rd_rel[i] == ~Past(go_rd)[i])
+ comb += Assert(Rose(busy))
- # Property 6: Similarly, if rd_rel is asserted,
- # asserting go_die should make rd_rel be deasserted
-
- with m.If(Past(rd_rel) != 0):
- with m.If(Past(go_die)):
- comb += Assert(rd_rel == 0)
+ # Instructions should not be issued if busy == 1
+ with m.If(busy):
+ comb += Assume(issue == 0)
- comb += Cover(Fell(rd_rel))
+ # Property 2: Issue will only be raised for one
+ # 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)
+
+ # Property 3: Read request is sent, which is acknowledged
+ # through the scoreboard to the priority picker which
+ # generates one go_read at a time. One of those will
+ # eventually be this computation unit
+
+ # there cannot be a go_rd if rd_rel is clear
+ with m.If(rd_rel == 0):
+ comb += Assume(go_rd == 0)
+
+ # Property 4: Once Go_Read is set, the src1/src2/operand
+ # latch door shuts and the ALU is told to proceed
+
+ # When a go_rd is received for each operand, the data
+ # should be captured
+ with m.If(~Past(go_die)):
+ with m.If(Past(go_rd)[0] & Past(rd_rel)[0]):
+ comb += Assert(dut.alu.a == Past(dut.src1_i))
+ with m.If(Past(go_rd)[1] & Past(rd_rel)[1]):
+ comb += Assert(dut.alu.b == Past(dut.src2_i))
+
+ # Property 5: When the ALU pipeline is ready, this
+ # activates write_request release and the ALU's output is
+ # captured in a temporary register
+
+ # I can't see the actual temporary register, so I have to
+ # simulate it here. This will be checked when the ALU data
+ # is actually output
+ alu_temp = Signal(16)
+ write_req_valid = Signal(reset=0)
+ with m.If(~Past(go_die) & Past(busy)):
+ with m.If(Rose(dut.alu.n.valid_o)):
+ sync += alu_temp.eq(dut.alu.o)
+ sync += write_req_valid.eq(1)
+
+ # write_req_valid should only be high once the alu finishes
+ with m.If(~write_req_valid & ~dut.alu.n.valid_o):
+ comb += Assert(wr_rel == 0)
- # Property 7: Similar to property 3, wr_rel should
- # never be asserted unless there was a preceeding issue
+ # Property 6: Write request release is held up if shadow_n
+ # is asserted low
- with m.If(wr_rel != 0):
- comb += Assert(has_issued)
+ # If shadow_n is low (indicating that everything is
+ # shadowed), wr_rel should not be able to rise
+ with m.If(shadow_n == 0):
+ with m.If(Past(wr_rel) == 0):
+ comb += Assert(wr_rel == 0)
- # Property 8: Similar to property 4, wr_rel should stay
- # asserted until a go_rd, go_die, or shadow
+ # Property 7: Write request release will go through a
+ # similar process as read request, resulting (eventually
+ # in go_write being asserted
- with m.If((Past(go_wr) == 0) & ~Past(go_die, 2) &
- ~Past(shadow)):
- comb += Assert(~Fell(wr_rel))
- # Assume go_wr is not asserted unless wr_rel is
+ # Go_wr should not be asserted if wr_rel is not
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
+ # is cleared, busy is dropped, and the comp unit is ready
+ # to do another task
- # Property 9: Similar to property 5, when wr_rel is
- # asserted and go_wr is asserted, then wr_rel should be
- # deasserted
+ # If a write release is accepted (by asserting go_wr),
+ # 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))
+ # 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)
- # Property 10: Similar to property 6, wr_rel should be
- # deasserted when go_die is asserted
- with m.If(Past(wr_rel) & Past(go_die)):
- comb += Assert(wr_rel == 0)
+ # It is REQUIRED that GO_Read be held valid only for one
+ # cycle, and it is REQUIRED that the corresponding read_req be
+ # dropped exactly one cycle after go_read is asserted high
- # Property 11: wr_rel should not fall while shadow is
- # asserted
- with m.If(wr_rel & shadow):
- comb += Assert(~Fell(wr_rel))
+ for i in range(2):
+ with m.If(Past(go_rd)[i] & Past(rd_rel)[i]):
+ comb += Assume(go_rd[i] == 0)
+ comb += Assert(rd_rel[i] == 0)
- # Assume no instruction is issued until rd_rel is
- # released. Idk if this is valid
+ # Likewise for go_write/wr_rel
+ with m.If(Past(go_wr) & Past(wr_rel)):
+ comb += Assume(go_wr == 0)
+ comb += Assert(wr_rel == 0)
- with m.If(busy):
- comb += Assume(issue == 0)
+ # When go_die is asserted the the entire FSM should be fully
+ # reset.
+
+ with m.If(Past(go_die) & Past(busy)):
+ comb += Assert(rd_rel == 0)
+ # this doesn't work?
+ # comb += Assert(wr_rel == 0)
+ sync += write_req_valid.eq(0)
return m
+
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=5)
- self.assertFormal(module, mode="cover", depth=5)
+ 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)
projects / soc.git / blobdiff