X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;ds=sidebyside;f=src%2Fsoc%2Ffu%2Fcompunits%2Fformal%2Fproof_fu.py;h=0af6ea6437ea501ff4441f0bd2c08361d5110997;hb=5bc4a63a1cfe6bdb76fd1d622d9f9565077beff2;hp=340510e127dcd2bd702ba4ece4dacdb71df67e29;hpb=27ca385067a6f9db3b73dda16542db452a261550;p=soc.git diff --git a/src/soc/fu/compunits/formal/proof_fu.py b/src/soc/fu/compunits/formal/proof_fu.py index 340510e1..0af6ea64 100644 --- a/src/soc/fu/compunits/formal/proof_fu.py +++ b/src/soc/fu/compunits/formal/proof_fu.py @@ -4,19 +4,21 @@ # 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): @@ -26,21 +28,26 @@ 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 = dut.shadown_i + shadow_n = dut.shadown_i rst = ResetSignal() @@ -48,111 +55,191 @@ class Driver(Elaboratable): 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]) - - # Property 6: Similarly, if rd_rel is asserted, - # asserting go_die should make rd_rel be deasserted + comb += Assert(Rose(busy)) - 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)