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()
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
projects / soc.git / commitdiff