LBDR Checker Extraction

Lower level checkers:

We can see that these cases are available for LBDR:

• if (flit = header and empty = 1) then all request should keep the previous value

• if (flit = Tail) then all requests should be Zero

• if (flit /= Header and flit /= Tail) then all request should keep the previous value

• We can find 8 checkers that checks the properties of N1, E1, W1 and S1 (shown with arrows)

  • if dst_addr(NoC_size-1 downto NoC_size/2) < cur_addr(NoC_size-1 downto NoC_size/2) then N1 should be 1
  • if dst_addr(NoC_size-1 downto NoC_size/2) >= cur_addr(NoC_size-1 downto NoC_size/2) then N1 should be 0
  • if cur_addr((NoC_size/2)-1 downto 0) < dst_addr((NoC_size/2)-1 downto 0) then E should be 1
  • if cur_addr((NoC_size/2)-1 downto 0) >= dst_addr((NoC_size/2)-1 downto 0) then E should be 0
  • if dst_addr((NoC_size/2)-1 downto 0) < cur_addr((NoC_size/2)-1 downto 0) then W should be 1
  • if dst_addr((NoC_size/2)-1 downto 0) >= cur_addr((NoC_size/2)-1 downto 0) then W should be 0
  • if cur_addr(NoC_size-1 downto NoC_size/2) < dst_addr(NoC_size-1 downto NoC_size/2) then S1 should be 1
  • if cur_addr(NoC_size-1 downto NoC_size/2) >= dst_addr(NoC_size-1 downto NoC_size/2) then S1 should be 0

• if flit_type = "001" and empty = '0' then Req_N_in should be equal to (N1_out and not E1_out and not W1_out)

• if flit_type = "001" and empty = '0' then Req_E_in should be equal to ((E1_out and not N1_out and not S1_out) or (E1_out and N1_out) or (E1_out and S1_out)))

• if flit_type = "001" and empty = '0' then Req_W_in should be equal to ((W1_out and not N1_out and not S1_out) or (W1_out and N1_out) or (W1_out and S1_out)) )

• if flit_type = "001" and empty = '0' then Req_S_in should be equal to (S1_out and not E1_out and not W1_out)

• if ( flit_type = "001" and empty = '0' then Req_L_in should be equal to (not N1_out and not E1_out and not W1_out and not S1_out) )

Higher level checkers

as an extension, we can have higher level checkers, please note that these checkers aren't directly extracted from the flow charts and they are not checking structural properties but they are more abstract:

• if (flit = header and empty = 0) then requests should be one hot
• if flit_type is header and empty is 0 and cur_addr = dst_addr then Req_L_in should be '1'

proposal for high level checkers

• if flit_type is header and empty is 0 and destination is on the west side of the current node, then request Req_W_in should be 1 and the rest 0
• if flit_type is header and empty is 0 and destination is on the east side of the current node, then request Req_E_in should be 1 and the rest 0
• if flit_type is header and empty is 0 and destination is on the north of the current node and not on east and not on west, then request Req_N_in should be 1 and the rest 0
• if flit_type is header and empty is 0 and destination is on the south of the current node and not on east and not on west, then request Req_S_in should be 1 and the rest 0