| | 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 | }}} |