Аноним

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

Материал из WEGA
 
(не показано 11 промежуточных версий 1 участника)
Строка 6: Строка 6:




Формальное определение задачи выглядит следующим образом. Пусть дан ориентированный граф <math>G = (V, E) \;</math>, представляющий схему в котором каждая вершина <math>v \in V \;</math> представляет вентиль, а каждое ребро <math>e \in E \;</math> – передачу сигнала от одного вентиля к другому с задержками <math>d: V \to \mathbb{R}^+ \;</math> и количествами регистров <math>w: E \to \mathbb{N} \;</math>. Целью задачи ресинхронизации с нахождением минимальной площади является перемещение регистров <math>w': E \to \mathbb{N} \;</math>, такое, что максимальная задержка между любыми двумя последовательными регистрами оказывается минимальной.
Формальное определение задачи выглядит следующим образом. Пусть дан ориентированный граф <math>G = (V, E) \;</math>, представляющий схему (в котором каждая вершина <math>v \in V \;</math> представляет вентиль, а каждое ребро <math>e \in E \;</math> – передачу сигнала от одного вентиля к другому) с задержками вентилей <math>d: V \to \mathbb{R}^+ \;</math> и количествами регистров <math>w: E \to \mathbb{N} \;</math>. Целью задачи ресинхронизации с нахождением минимальной длительности такта является перемещение регистров <math>w': E \to \mathbb{N} \;</math>, такое, что максимальная задержка между любыми двумя последовательными регистрами оказывается минимальной.


== Нотация ==
== Нотация ==
Строка 14: Строка 14:




Кроме того, чтобы избежать явного перечисления путей при поиске самого длинного пути, еще одна метка <math>t: V \to \mathbb{R}^+ \;</math> будет представлять выходное время прибытия каждого вентиля – иначе говоря, максимальную задержку вентиля при взгляде из любого предшествующего регистра. Для того чтобы t было не меньше комбинационной задержки, должно выполняться условие
Кроме того, чтобы избежать явного перечисления путей при поиске самого длинного пути, еще одна метка <math>t: V \to \mathbb{R}^+ \;</math> будет представлять выходное время прибытия каждого вентиля – иначе говоря, максимальную задержку вентиля при переходе из любого предшествующего регистра. Для того чтобы t было не меньше комбинационной задержки, должно выполняться условие


<math>\forall (u, v) \in E: w'[u, v] = 0 \Rightarrow t[v] \ge t[u] + d[v] \;</math>.
<math>\forall (u, v) \in E: w'[u, v] = 0 \Rightarrow t[v] \ge t[u] + d[v] \;</math>.


== Ограничения и цель ==
== Ограничения и цель ==
В силу данной нотации допустимая ресинхронизация r не должна иметь отрицательного количества регистров по какому-либо ребру. Подобное условие допустимости задается формулой  
В данной нотации допустимая ресинхронизация r не должна иметь отрицательного количества регистров по какому-либо ребру. Подобное условие допустимости задается формулой  


<math>P0(r) \triangleq  \forall (u, v) \in E: w[u, v] + r[v] - r[u] \ge 0 \;</math>.
<math>P0(r) \triangleq  \forall (u, v) \in E: w[u, v] + r[v] - r[u] \ge 0 \;</math>.
Строка 36: Строка 36:




Ресинхронизация с достижением минимальной длительности представляет собой решение задачи <math>\langle r, t \rangle \;</math>, удовлетворяющее следующему условию оптимальности:
Ресинхронизация с достижением минимальной длительности представляет собой решение <math>\langle r, t \rangle \;</math>, удовлетворяющее следующему условию оптимальности:


<math>P3 \triangleq \forall r', t': P(r', t') \implies max(t) \le max(t') \;</math>, где <math>max(t) \triangleq max_{v \in V} t[v] \;</math>.
<math>P3 \triangleq \forall r', t': P(r', t') \implies max(t) \le max(t') \;</math>, где <math>max(t) \triangleq max_{v \in V} \; t[v]</math>.




Строка 85: Строка 85:




Однако подобная ASAP-операция может ускорить r[u] даже в случае w[u, v] - r[u] + r[v] = 0 для ребра (u, v). Это означает, что P0 может быть уже не инвариантом. Однако перемещение P0 из инварианта в цель цикла не составит проблемы, поскольку для этого в цикл можно добавить одну команду:
Однако подобная ASAP-операция может увеличить r[u] даже в случае w[u, v] - r[u] + r[v] = 0 для ребра (u, v). Это означает, что P0 может быть уже не инвариантом. Однако перемещение P0 из инварианта в цель цикла не составит проблемы, поскольку для этого в цикл можно добавить одну команду:


<math>\exist (u, v) \in E: r[u] - r[v] > w[u, v] \to r[v] := r[u] - w[u, v] \;</math>.
<math>\exist (u, v) \in E: r[u] - r[v] > w[u, v] \to r[v] := r[u] - w[u, v] \;</math>.
Строка 94: Строка 94:
   <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>\neg P3 \and \exist v \in V: t[v] \ge \phi</math>
   <math>\neg P3 \and \exist \; v \in V: t[v] \ge \phi</math>
   <math>\to r[v], t[v] := r[v] + 1, d[v]</math>
   <math>\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>




Строка 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>.
Строка 254: Строка 254:


== Применение ==
== Применение ==
В базовом алгоритме оптимальность P3 проверяется условием r[v] > j Vj. Однако в большинстве случаев условие оптимальности можно обнаружить намного раньше. Поскольку при каждом возрастании r[v] должна существовать «вершина-хранитель» u, такая, что после выполнения действия будет верно неравенство r[u] — r0[u] > r[v] — r0 [v].  
В базовом алгоритме оптимальность P3 проверяется условием <math>r[v] \ge |V| \;</math>. Однако в большинстве случаев условие оптимальности можно обнаружить намного раньше. Поскольку при каждом возрастании r[v] должна существовать «вершина-хранитель» u, такая, что после выполнения действия будет верно неравенство <math>r[u] - r'[u] \ge r[v] - r'[v] \;</math>. Следовательно, если ввести указатель из v на u при увеличении r[v], указатели не смогут образовать цикл согласно <math>\neg P3</math>. Фактически указатели образуют лес, в котором корни имеют значение r = 0, а потомок может иметь значение r, не более чем на 1 превышающее значение его предка. Использование цикла указателей как свидетельство верности P3 вместо <math>r[v] \ge |V| \;</math>, можно значительно повысить практическую эффективность алгоритма.


== Открытые вопросы ==
Ресинхронизация обычно используется для оптимизации длительности цикла либо количества регистров в схеме. Описанный алгоритм решает только задачу ресинхронизации с достижением минимальной длительности. Задачу ресинхронизации с достижением минимального количества регистров для заданной длительности цикла решили Лейзерсон и Сакс [1], она представлена в соответствующей статье. Их алгоритм сводит задачу к двойственной проблеме поиска сетевого потока с минимальной стоимостью в плотном графе. Остается открытым любопытный вопрос – можно ли разработать эффективный итеративный алгоритм для решения задачи о минимальном количестве регистров, схожий с алгоритмом Чжоу.


Следовательно, если ввести указатель из v к u при увеличении r[v], указатели не смогут образовать цикл согласно :P3. Фактически указатели образуют лес, в котором корни имеют значение r = 0, а потомок может иметь значение r, не более чем на 1 превышающее значение его предка. Использование цикла указателей как свидетельство верности P3 вместо r[v] > |V|, можно значительно повысить практическую эффективность алгоритма.
== Открытые вопросы ==
Ресинхронизация нередко используется для оптимизации длительности цикла либо количества регистров в схеме. Описанный алгоритм решает только задачу ресинхронизации с достижением минимальной длительности. Задачу ресинхронизации с достижением минимального количества регистров для заданной длительности цикла решили Лейзерсон и Сакс [1], она представлена в соответствующей статье. Их алгоритм сводит задачу к двойственной проблеме поиска сетевого потока с минимальной стоимостью в плотном графе. Остается открытым любопытный вопрос – можно ли разработать эффективный итеративный алгоритм для решения задачи о минимальном количестве регистров, схожий с алгоритмом Чжоу.
== Экспериментальные результаты ==
== Экспериментальные результаты ==
Результаты были опубликованы Чжоу [3] по итогам сравнения времени выполнения алгоритма с эффективной эвристикой под названием ASTRA [ ]. Результаты прогона на эталонных тестах ISCAS89 представлены в таблице 1 из работы [3]; столбцы A и B таблицы отражают время выполнения двух этапов ASTRA.
Результаты были опубликованы Чжоу [3] по итогам сравнения времени выполнения алгоритма с эффективной эвристикой под названием ASTRA [2]. Результаты прогона на эталонных тестах ISCAS89 представлены в таблице 1 из работы [3]; столбцы A и B таблицы отражают время выполнения двух этапов ASTRA.


== См. также ==
== См. также ==
Строка 274: Строка 271:


3. Zhou, H.: Deriving a new efficient algorithm for min-period retiming. In: Asia and South Pacific Design Automation Conference, Shanghai, China, January 2005
3. Zhou, H.: Deriving a new efficient algorithm for min-period retiming. In: Asia and South Pacific Design Automation Conference, Shanghai, China, January 2005
[[Категория: Совместное определение связанных терминов]]