| 286 | What is to be proven : If a vci_transaction (local) waits on the external_crossbar (TSAR), it will be arbitrated. |
| 287 | If the vci_transaction is global, the local external_crossbar input will have a greater time due to the null_response treatment. |
| 288 | If there is more than one vci_transaction, the cluster the lowest one is considered, the others are already allowing the arbitration and can be neglect. |
| 289 | |
| 290 | {{{#!c++ |
| 291 | //Qqt : quantum targets - Qqlc : quantum local crossbar - Qqgc : quantum global crossbar |
| 292 | //Δlocal - Δglobal : routing delays |
| 293 | //EC : External_crossbar |
| 294 | //C : Cluster which transmitted the transaction and need arbitration |
| 295 | }}} |
| 296 | {{{#!c++ |
| 297 | //Demonstrating that with condition : for every cluster else than C : |
| 298 | T.EC_input > T.EC_input.C |
| 299 | |
| 300 | //Time of the pending request |
| 301 | T.EC_input.C = minT.C.initiator = minT.global_crossbar_inputs - Δlocal //due to null_responses |
| 302 | |
| 303 | //Condition for locking the cluster : |
| 304 | minT.initiator + Δlocal > minT.global_crossbar_inputs + Qqgc |
| 305 | minT.initiator > T.EC_input.C + Qqgc |
| 306 | |
| 307 | //Condition for a memory cache to get a temporal information |
| 308 | T.local_crossbar.memory_cache_output +Qqlc <= T.local_crossbar |
| 309 | T.local_crossbar - Qqlc >= T.memory_cache |
| 310 | |
| 311 | //Condition for an input from the external_crossbar to get a temporal information |
| 312 | T.memory_cache.EC_output + Qqt <= T.memory_cache |
| 313 | T.memory_cache - Qqt >= T.EC_input |
| 314 | T.local_crossbar - Qqlc - Qqt >= T.memory_cache - Qqt >= T.EC_input |
| 315 | |
| 316 | //minimum timer without update |
| 317 | minT.EC_input = T.local_crossbar - Qqlc - Qqt + 1 |
| 318 | |
| 319 | //The clusters are locked |
| 320 | T.local_crossbar > T.EC_input.C + Qqgc |
| 321 | T.local_crossbar - Qqlc - Qqt + 1 > T.EC_input.C + Qqgc - Qqlc - Qqt + 1 |
| 322 | minT.EC_input > T.EC_input.C + Qqgc - (Qqlc + Qqt) +1 |
| 323 | |
| 324 | Then if Qqgc - (Qqlc + Qqt) + 1 > 0 , The inequality -- minT.EC_input > T.EC_input.C -- is true too |
| 325 | |
| 326 | Thus |
| 327 | |
| 328 | Qqgc - (Qqlc + Qqt) + 1 > 0 |
| 329 | Qqgc > Qqlc + Qqt - 1 |
| 330 | ------------------- |
| 331 | Qqgc >= Qqlc + Qqt |
| 332 | ------------------- |
| 333 | |
| 334 | QED |
| 335 | |
| 336 | }}} |