Аноним

Ресинхронизация схемы: инкрементный подход: различия между версиями

Материал из WEGA
м
Строка 101: Строка 101:
   <math>\exist \; (u, v) \in E: r[u] - r[v] > w[u, v]</math>
   <math>\exist \; (u, v) \in E: r[u] - r[v] > w[u, v]</math>
   <math>\to r[v] := r[u] - w[u, v]</math>
   <math>\to r[v] := r[u] - w[u, v]</math>
   <math>od \{ P0 \and P1 \and P2 \and P3 \} \;</math>.
   <math>od \{ P0 \and P1 \and P2 \and P3 \}. \;</math>




Строка 107: Строка 107:
|-
|-
! Название
! Название
! Кол-во вентилей
! Кол-во
! colspan="2" | Длительность такта
! colspan="2" | Длительность такта
! <math>\sum r</math>
! <math>\sum r</math>
! Кол-во обновлений
! Кол-во
! Время  
! Время  
! colspan="2" | ASTRA
! colspan="2" | ASTRA
|-
|-
!  
!  
!  
! вентилей
! до
! до
! после
! после
!  
!  
!  
! обновлений
!  
!  
! A(s)
! A(s)
Строка 229: Строка 229:




Для завершения разработки алгоритма осталось реализовать проверку <math>\neg P3</math>. Из предыдущего обсуждения мы уже знаем, что из <math>\neg P3</math> следует, что существует такая вершина u, что <math>r[u] - r'[u] \ge r[v] - r'[v] \;</math> после каждого увеличения r[v]. Это означает, что <math>max_{v \in V} \; r[v] - r'[v]</math> не будет увеличиваться. Иначе говоря, существует по меньшей мере одна вершина v, у которой r[v] не будет меняться. До увеличения r[v] имеет место соотношение <math>w_{u \rightsquigarrow v} - r[u] + r[v] \le 0 \;</math>, где <math>w_{u \rightsquigarrow v} \ge 0 \;</math> – исходное количество регистров на одной пути из u в v, в результате чего неравенство <math>r[v] - r[u] \le 1 \;</math> остается верным даже после увеличения r[v]. Из этого следует, что будет по меньшей мере i + 1 вершин, у которых r не превышает i для <math>0 \le i < |V| \;</math>. Иными словами, алгоритм может по-прежнему увеличивать r, и когда какое-либо значение r достигнет |V|, это покажет, что условие P3 удовлетворяется. Таким образом, полный алгоритм имеет следующую форму:
Для завершения разработки алгоритма осталось реализовать проверку <math>\neg P3</math>. Из предыдущего обсуждения мы уже знаем, что из <math>\neg P3</math> следует, что существует такая вершина u, что <math>r[u] - r'[u] \ge r[v] - r'[v] \;</math> после каждого увеличения r[v]. Это означает, что <math>max_{v \in V} \; r[v] - r'[v]</math> не будет увеличиваться. Иначе говоря, существует по меньшей мере одна вершина v, у которой r[v] не будет меняться. До увеличения r[v] имеет место соотношение <math>w_{u \rightsquigarrow v} - r[u] + r[v] \le 0 \;</math>, где <math>w_{u \rightsquigarrow v} \ge 0 \;</math> – исходное количество регистров на одном пути из u в v, в результате чего неравенство <math>r[v] - r[u] \le 1 \;</math> остается верным даже после увеличения r[v]. Из этого следует, что будет по меньшей мере i + 1 вершин, у которых r не превышает i для <math>0 \le i < |V| \;</math>. Иными словами, алгоритм может по-прежнему увеличивать r, и когда какое-либо значение r достигнет |V|, это покажет, что условие P3 удовлетворяется. Таким образом, полный алгоритм имеет следующую форму:


   <math>r, t, \phi := 0, d, \infty \;</math>
   <math>r, t, \phi := 0, d, \infty \;</math>
   do {P1}
   do {P1}
   <math>\exist (u, v) \in E: r[u] - r[v] = w[u, v]</math>
   <math>\exist \; (u, v) \in E: r[u] - r[v] = w[u, v]</math>
   <math>\and \; t[v] - t[u] < d[v] \to t[v] := t[u] + d[v]</math>
   <math>\and \; t[v] - t[u] < d[v] \to t[v] := t[u] + d[v]</math>
   <math>(\forall \; v \in V: r[v] < |V|)</math>
   <math>(\forall \; v \in V: r[v] < |V|)</math>
Строка 240: Строка 240:
   <math>\and \; \exist \; v \in V: t[v] \ge \phi \to r[v], t[v] := r[v] + 1, d[v]</math>
   <math>\and \; \exist \; v \in V: t[v] \ge \phi \to r[v], t[v] := r[v] + 1, d[v]</math>
   <math>P0 \and P2 \and \phi > max(t) \to \phi := max(t)</math>
   <math>P0 \and P2 \and \phi > max(t) \to \phi := max(t)</math>
   <math>\exist (u, v) \in E: r[u] - r[v] > w[u, v]</math>
   <math>\exist \; (u, v) \in E: r[u] - r[v] > w[u, v]</math>
   <math>\to r[v] := r[u] - w[u, v]</math>
   <math>\to r[v] := r[u] - w[u, v]</math>
   <math>od \{ P0 \and P1 \and P2 \and P3 \} \;</math>.
   <math>od \{ P0 \and P1 \and P2 \and P3 \} \;</math>.
4551

правка