From 69f32081ba4047e855f0ea5a8107266db7a11a95 Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Tue, 26 May 2020 13:33:19 -0400 Subject: [PATCH] Rewrite proof to be more in line with what appears in the wiki --- src/soc/fu/compunits/formal/proof_fu.py | 160 +++++++++++++----------- 1 file changed, 84 insertions(+), 76 deletions(-) diff --git a/src/soc/fu/compunits/formal/proof_fu.py b/src/soc/fu/compunits/formal/proof_fu.py index c2b964c5..d149fae6 100644 --- a/src/soc/fu/compunits/formal/proof_fu.py +++ b/src/soc/fu/compunits/formal/proof_fu.py @@ -39,8 +39,7 @@ class Driver(Elaboratable): wr_rel = dut.wr.rel go_die = dut.go_die_i - shadow = Signal() - comb += shadow.eq(~dut.shadown_i) + shadow_n = dut.shadown_i rst = ResetSignal() @@ -56,95 +55,104 @@ class Driver(Elaboratable): 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) + comb += Assert(Rose(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 + # Instructions should not be issued if busy == 1 + with m.If(busy): + comb += Assume(issue == 0) - with m.If(Past(rd_rel) != 0): - with m.If(Past(go_die)): - comb += Assert(rd_rel == 0) + # Property 2: Issue will only be raised for one + # cycle. Read requests may go out immediately after issue + # goes low - comb += Cover(Fell(rd_rel)) + # issue can only be raised for one cycle + with m.If(Past(issue)): + comb += Assume(issue == 0) + + # 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)) + comb += Assert(rd_rel[0] == 0) + 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(Past(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 or go_die + # 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, 1) & - ~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 9: Similar to property 5, when wr_rel is - # asserted and go_wr is asserted, then wr_rel should be - # deasserted - with m.If(Past(wr_rel) & Past(go_wr)): - comb += Assert(wr_rel == 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) - # Property 11: wr_rel should not fall while shadow is - # asserted - with m.If(wr_rel & shadow): - comb += Assert(~Fell(wr_rel)) + # 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 - # Assume no instruction is issued until rd_rel is - # released. Idk if this is valid - # (lkcl notes: it's actually that no instruction is issued - # until *busy* is released. oh i think i see what you - # mean: well... kinda. because rd_rel relies on wr_rel - # and wr_rel relies on instruction, there exists a - # transitive relationship, which is not strictly necessary to - # explicitly check) + # 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) + # wr_rel is dropped + comb += Assert(wr_rel == 0) + # busy is dropped. + with m.If(~Past(go_die)): + comb += Assert(busy == 0) - with m.If(busy): - comb += Assume(issue == 0) return m -- 2.30.2