Ресинхронизация схемы: инкрементный подход: различия между версиями
Irina (обсуждение | вклад) |
Irina (обсуждение | вклад) |
||
(не показано 18 промежуточных версий этого же участника) | |||
Строка 6: | Строка 6: | ||
Формальное определение задачи выглядит следующим образом. Пусть дан ориентированный граф <math>G = (V, E) \;</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> будет представлять выходное время прибытия каждого вентиля – иначе говоря, максимальную задержку вентиля при | Кроме того, чтобы избежать явного перечисления путей при поиске самого длинного пути, еще одна метка <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 не должна иметь отрицательного количества регистров по какому-либо ребру. Подобное условие допустимости задается формулой | ||
<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>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>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>. | ||
Строка 60: | Строка 60: | ||
<math> \neg P2 \to update \; t</math> | <math> \neg P2 \to update \; t</math> | ||
<math> \neg P3 \to update \; r</math> | <math> \neg P3 \to update \; r</math> | ||
od <math>\{ P0 \and P1 \and P2 \and P3 \} \;</math>. | |||
Первую команду цикла можно переписать в виде <math>\exist (u, v) \in E: r[u] - r[v] = w[u, v] \and t[v] - t[u] < d[v] \to t[v] := t[u] + d[v] \;</math>. | Первую команду цикла можно переписать в виде <math>\exist (u, v) \in E: r[u] - r[v] = w[u, v] \and t[v] - t[u] < d[v] \to t[v] := t[u] + d[v] \;</math>. | ||
Строка 68: | Строка 68: | ||
Вторая | Вторая команда не так проста. Если <math>\neg P3 \;</math>, иначе говоря, если существует другая допустимая ресинхронизация <math>\langle r', t' \rangle \;</math>, такая, что max(t) > max(t'), тогда на любой вершине v, для которой выполняется t[v] = max(t), должно выполняться соотношение t'[v] < t[v]. Для этих вершин известно следующее свойство: | ||
=> ( | <math>\forall v \in V: t'[v] < t[v] => (\exist u \in V: r[u] - r[v] > r'[u] - r'[v]) \;</math>, | ||
что означает, что если время прибытия вершины v меньше при другой ресинхронизации <math>\langle r', t' \rangle \;</math>, тогда должна существовать вершина u, такая, что r' обеспечивает больше регистров между u и v. Фактически одной такой вершиной u является начальная вершина самого длинного комбинационного пути к v, дающего задержку t[v]. | |||
что | Для сокращения длительности цикла переменную r необходимо изменить, сделав ее ближе к r'. Следует отметить, что в контексте ресинхронизации важны не абсолютные значения r, но их разности. Если <math>\langle r, t \rangle \;</math> является решением задачи ресинхронизации, то <math>\langle r + c, t \rangle \;</math>, где <math>c \in \mathbb{Z} \;</math> – произвольная константа, также будет являться решением. Следовательно, r может быть сделана «ближе» к r' за счет размещения большего количества регистров между u и v, то есть либо за счет уменьшения r[u], либо за счет увеличения r[v]. Отметим, что v можно легко определить из соотношения t[v] = max(t). Независимо от того, какое значение (r[v] или r[u]) выбрано для изменения, изменение должно быть единичным, поскольку r не следует чрезмерно корректировать. Таким образом, после корректировки будут по-прежнему выполняться соотношения <math>r[v] - r[u] \le r'[v] - r'[u] \;</math> или, что эквивалентно, <math>r[v] - r'[v] \le r[u] - r'[u] \;</math>. Поскольку v легко определить, выберем для увеличения r[v]. Время прибытия t[v] можно незамедлительно уменьшить до d[v]. Это позволяет уточнить вторую команду: | ||
<math>\neg P3 \and P2 \and \exist v \in V: t[v] = max(t) \to r[v], t[v] :=r[v] + 1, d[v] \;</math>. | |||
Поскольку во время выполнения этой операции регистры перемещаются, предикат P2 может перестать выполняться. Однако первая команда восстановит статус кво. Эта команда увеличивает t для некоторых вершин; некоторые из них даже могут превысить значение max(t) до перемещения регистра. Аналогичное рассуждение для <math>\langle r, t \rangle \;</math> показывает, что их значения r также подвергаются увеличению. Таким образом, для реализации данного «насколько возможно быстрого» (As-Soon-As-Possible, ASAP) увеличения r необходимо сделать моментальный снимок max(t), пока предикат P2 еще актуален. Физически такой моментальный снимок записывает один такт применимой длительности <math>\phi \;</math> и может быть реализован при помощи добавления к циклу еще одной команды: | |||
<math>P2 \and \phi > max(t) \to \phi := max(t) \;</math>. | |||
Однако подобная ASAP-операция может | Однако подобная 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>r, t, \phi := 0, d, \infty \;</math> | |||
do {P1} | |||
<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>\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>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>\to r[v] := r[u] - w[u, v]</math> | |||
<math>od \{ P0 \and P1 \and P2 \and P3 \}. \;</math> | |||
{| class="wikitable" | |||
|- | |||
! Название | |||
! Кол-во | |||
! colspan="2" | Длительность такта | |||
! <math>\sum r</math> | |||
! Кол-во | |||
! Время | |||
! colspan="2" | ASTRA | |||
|- | |||
! | |||
! вентилей | |||
! до | |||
! после | |||
! | |||
! обновлений | |||
! | |||
! A(s) | |||
! B(s) | |||
|- | |||
| s1423 | |||
| 490 | |||
| 166 | |||
| 127 | |||
| 808 | |||
| 7619 | |||
| 0,02 | |||
| 0,03 | |||
| 0,02 | |||
|- | |||
| s1494 | |||
| 558 | |||
| 89 | |||
| 88 | |||
| 628 | |||
| 7765 | |||
| 0,02 | |||
| 0,01 | |||
| 0,01 | |||
|- | |||
| s9234 | |||
| 2027 | |||
| 89 | |||
| 81 | |||
| 2215 | |||
| 76943 | |||
| 0,12 | |||
| 0,11 | |||
| 0,09 | |||
|- | |||
| s9234.1 | |||
| 2027 | |||
| 89 | |||
| 81 | |||
| 2164 | |||
| 77644 | |||
| 0,16 | |||
| 0,11 | |||
| 0,10 | |||
|- | |||
| s13207 | |||
| 2573 | |||
| 143 | |||
| 82 | |||
| 4086 | |||
| 28395 | |||
| 0,12 | |||
| 0,38 | |||
| 0,12 | |||
|- | |||
| s15850 | |||
| 3448 | |||
| 186 | |||
| 77 | |||
| 12038 | |||
| 99314 | |||
| 0,36 | |||
| 0,43 | |||
| 0,17 | |||
|- | |||
| s35932 | |||
| 12204 | |||
| 109 | |||
| 100 | |||
| 16373 | |||
| 108459 | |||
| 0,28 | |||
| 0,24 | |||
| 0,65 | |||
|- | |||
| s38417 | |||
| 8709 | |||
| 110 | |||
| 56 | |||
| 9834 | |||
| 155489 | |||
| 0,58 | |||
| 0,89 | |||
| 0,64 | |||
|- | |||
| s38584 | |||
| 11448 | |||
| 191 | |||
| 163 | |||
| 19692 | |||
| 155637 | |||
| 0,41 | |||
| 0,50 | |||
| 0,67 | |||
|- | |||
| s38584.1 | |||
| 11448 | |||
| 191 | |||
| 183 | |||
| 9416 | |||
| 114940 | |||
| 0,48 | |||
| 0,55 | |||
| 0,78 | |||
|} | |||
Таблица 1. Экспериментальные результаты | Таблица 1. Экспериментальные результаты | ||
Для завершения разработки алгоритма осталось реализовать проверку | Для завершения разработки алгоритма осталось реализовать проверку <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> | |||
do {P1} | |||
<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>(\forall \; v \in V: r[v] < |V|)</math> | |||
<math>\and \; \exist \; v \in V: t[v] \ge \phi \to r[v], t[v] := r[v] + 1, d[v]</math> | |||
<math>(\exist \; v \in V: r[v] \ge |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>\exist \; (u, v) \in E: r[u] - r[v] > w[u, v]</math> | |||
<math>\to r[v] := r[u] - w[u, v]</math> | |||
<math>od \{ P0 \and P1 \and P2 \and P3 \} \;</math>. | |||
Корректность алгоритма можно легко показать в силу того, что P1 остается инвариантом и из отрицания предикатов следует <math>P0 \and P2 \and P3 \;</math>. Завершение работы алгоритма гарантируется монотонным возрастанием r и его верхней границей. Следующая теорема задает время выполнения в наихудшем случае. | |||
Время выполнения алгоритма ресинхронизации в наихудшем случае | '''Теорема 1. Время выполнения данного алгоритма ресинхронизации в наихудшем случае ограничено сверху значением <math>O(|V|^2 \; |E|)</math>.''' | ||
Время выполнения алгоритма ресинхронизации в наихудшем случае будет актуальным в случае, когда каждое увеличение r приводит к «протягиванию» синхронизации по всей схеме (т.е. по |E| ребрам). Это верно только тогда, когда увеличение r перемещает все регистры в схеме. Однако в таком случае верхняя граница r равна 1, и время выполнения не превышает O(|V| |E|). С другой стороны, если значение r велико, схема разбивается регистрами на несколько меньших фрагментов, в результате чего протягивание, вызванное увеличением одного r, ограничено деревом небольшого размера. | |||
Следовательно, если ввести указатель из 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], она представлена в соответствующей статье. Их алгоритм сводит задачу к двойственной проблеме поиска сетевого потока с минимальной стоимостью в плотном графе. Остается открытым любопытный вопрос – можно ли разработать эффективный итеративный алгоритм для решения задачи о минимальном количестве регистров, схожий с алгоритмом Чжоу. | ||
== Экспериментальные результаты == | == Экспериментальные результаты == | ||
Результаты были опубликованы Чжоу [3] по итогам сравнения времени выполнения алгоритма с эффективной эвристикой под названием ASTRA [ ]. Результаты прогона на эталонных тестах ISCAS89 представлены в таблице 1 из работы [3]; столбцы A и B таблицы отражают время выполнения двух этапов ASTRA. | Результаты были опубликованы Чжоу [3] по итогам сравнения времени выполнения алгоритма с эффективной эвристикой под названием ASTRA [2]. Результаты прогона на эталонных тестах ISCAS89 представлены в таблице 1 из работы [3]; столбцы A и B таблицы отражают время выполнения двух этапов ASTRA. | ||
== См. также == | == См. также == |
Текущая версия от 15:11, 3 июля 2017
Ключевые слова и синонимы
Ресинхронизация с достижением минимальной длительности
Постановка задачи
Ресинхронизация схемы является одной из самых эффективных техник структурной оптимизации для последовательных схем. Она перемещает регистры внутри схемы, не меняя ее функции. Задача ресинхронизации с достижением минимальной длительности стремится минимизировать самую долгую задержку между любыми двумя последовательными регистрами, которая определяет длительность такта.
Формальное определение задачи выглядит следующим образом. Пусть дан ориентированный граф [math]\displaystyle{ G = (V, E) \; }[/math], представляющий схему (в котором каждая вершина [math]\displaystyle{ v \in V \; }[/math] представляет вентиль, а каждое ребро [math]\displaystyle{ e \in E \; }[/math] – передачу сигнала от одного вентиля к другому) с задержками вентилей [math]\displaystyle{ d: V \to \mathbb{R}^+ \; }[/math] и количествами регистров [math]\displaystyle{ w: E \to \mathbb{N} \; }[/math]. Целью задачи ресинхронизации с нахождением минимальной длительности такта является перемещение регистров [math]\displaystyle{ w': E \to \mathbb{N} \; }[/math], такое, что максимальная задержка между любыми двумя последовательными регистрами оказывается минимальной.
Нотация
Чтобы гарантировать, что новые регистры – это перемещенные старые, метка [math]\displaystyle{ r: V \to \mathbb{Z} \; }[/math] используется для обозначения того, сколько регистров перемещены из исходящих ребер каждой вершины на входящие. Используя эту нотацию, можно вычислить новое количество регистров ребра (u, v) по формуле
[math]\displaystyle{ w'[u, v] = w[u, v] + r[v] - r[u] \; }[/math].
Кроме того, чтобы избежать явного перечисления путей при поиске самого длинного пути, еще одна метка [math]\displaystyle{ t: V \to \mathbb{R}^+ \; }[/math] будет представлять выходное время прибытия каждого вентиля – иначе говоря, максимальную задержку вентиля при переходе из любого предшествующего регистра. Для того чтобы t было не меньше комбинационной задержки, должно выполняться условие
[math]\displaystyle{ \forall (u, v) \in E: w'[u, v] = 0 \Rightarrow t[v] \ge t[u] + d[v] \; }[/math].
Ограничения и цель
В данной нотации допустимая ресинхронизация r не должна иметь отрицательного количества регистров по какому-либо ребру. Подобное условие допустимости задается формулой
[math]\displaystyle{ P0(r) \triangleq \forall (u, v) \in E: w[u, v] + r[v] - r[u] \ge 0 \; }[/math].
Как уже было установлено, условия, согласно которым t является допустимым временем прибытия, задаются следующими двумя предикатами.
[math]\displaystyle{ P1(t) \triangleq \forall v \in V: t[v] \ge d[v] \; }[/math],
[math]\displaystyle{ P2(r, t) \triangleq \forall u, v \in E: r[u] - r[v] = w[u, v] \implies t[v] - t[u] \ge d[v] \; }[/math].
Предикат P обозначает конъюнкцию двух вышеупомянутых условий:
[math]\displaystyle{ P(r, t) \triangleq P0(r) \and P1(t) \and P2(r, t) \; }[/math].
Ресинхронизация с достижением минимальной длительности представляет собой решение [math]\displaystyle{ \langle r, t \rangle \; }[/math], удовлетворяющее следующему условию оптимальности:
[math]\displaystyle{ P3 \triangleq \forall r', t': P(r', t') \implies max(t) \le max(t') \; }[/math], где [math]\displaystyle{ max(t) \triangleq max_{v \in V} \; t[v] }[/math].
Далее будет обсуждаться только допустимая ресинхронизация (r', t'), поэтому для упрощения изложения условие на диапазон P(r', t') часто будет опущено; значение будет очевидно из контекста.
Основные результаты
В данном разделе будет показано, как разработать эффективный алгоритм для решения задачи ресинхронизации с минимальной длительностью. В отличие от обычного стиля изложения, когда представлен только финальный продукт, т.е. алгоритм, но не идеи по его разработке, далее будет изложен поэтапный процесс, приводящий в конечном итоге к созданию алгоритма.
Разработка алгоритма заключается в построении процедуры, такой, что ее выполнение завершится через конечное число шагов, а при завершении она будет удовлетворять заданному предикату. В случае задачи ресинхронизации с минимальной длительностью должен удовлетворяться предикат [math]\displaystyle{ P0 \and P1 \and P2 \and P3 \; }[/math]. Этот предикат также называется постусловием. Можно утверждать, что любой нетривиальный алгоритм будет содержать по меньшей мере один цикл; в противном случае продолжительность обработки пропорциональна просто длине текста. Следовательно, некоторая часть постусловий будет итеративно удовлетворяться в цикле, тогда как оставшаяся часть будет изначально удовлетворяться в процессе инициализации и оставаться инвариантной во время выполнения цикла.
Первое решение, которое необходимо принять, касается разбиения постусловий на возможные инварианты цикла и его цель. Из четырех конъюнктивных членов предикат P3 задает условие оптимальности и является самым сложным из всех. Следовательно, он будет рассматриваться как цель при выполнении цикла. С другой стороны, предикаты P0 и P1 легко могут быть удовлетворены при помощи простой инициализации:
r, t := 0, d.
Основываясь на этих соображениях, мы планируем разработать алгоритм согласно следующей схеме.
r, t := 0, d do [math]\displaystyle{ \{ P0 \and P1 \} \; }[/math] [math]\displaystyle{ \neg P2 \to update \; t }[/math] [math]\displaystyle{ \neg P3 \to update \; r }[/math] od [math]\displaystyle{ \{ P0 \and P1 \and P2 \and P3 \} \; }[/math].
Первую команду цикла можно переписать в виде [math]\displaystyle{ \exist (u, v) \in E: r[u] - r[v] = w[u, v] \and t[v] - t[u] \lt d[v] \to t[v] := t[u] + d[v] \; }[/math].
Фактически это релаксация алгоритма Беллмана-Форда для вычисления самых длинных путей.
Вторая команда не так проста. Если [math]\displaystyle{ \neg P3 \; }[/math], иначе говоря, если существует другая допустимая ресинхронизация [math]\displaystyle{ \langle r', t' \rangle \; }[/math], такая, что max(t) > max(t'), тогда на любой вершине v, для которой выполняется t[v] = max(t), должно выполняться соотношение t'[v] < t[v]. Для этих вершин известно следующее свойство:
[math]\displaystyle{ \forall v \in V: t'[v] \lt t[v] =\gt (\exist u \in V: r[u] - r[v] \gt r'[u] - r'[v]) \; }[/math],
что означает, что если время прибытия вершины v меньше при другой ресинхронизации [math]\displaystyle{ \langle r', t' \rangle \; }[/math], тогда должна существовать вершина u, такая, что r' обеспечивает больше регистров между u и v. Фактически одной такой вершиной u является начальная вершина самого длинного комбинационного пути к v, дающего задержку t[v].
Для сокращения длительности цикла переменную r необходимо изменить, сделав ее ближе к r'. Следует отметить, что в контексте ресинхронизации важны не абсолютные значения r, но их разности. Если [math]\displaystyle{ \langle r, t \rangle \; }[/math] является решением задачи ресинхронизации, то [math]\displaystyle{ \langle r + c, t \rangle \; }[/math], где [math]\displaystyle{ c \in \mathbb{Z} \; }[/math] – произвольная константа, также будет являться решением. Следовательно, r может быть сделана «ближе» к r' за счет размещения большего количества регистров между u и v, то есть либо за счет уменьшения r[u], либо за счет увеличения r[v]. Отметим, что v можно легко определить из соотношения t[v] = max(t). Независимо от того, какое значение (r[v] или r[u]) выбрано для изменения, изменение должно быть единичным, поскольку r не следует чрезмерно корректировать. Таким образом, после корректировки будут по-прежнему выполняться соотношения [math]\displaystyle{ r[v] - r[u] \le r'[v] - r'[u] \; }[/math] или, что эквивалентно, [math]\displaystyle{ r[v] - r'[v] \le r[u] - r'[u] \; }[/math]. Поскольку v легко определить, выберем для увеличения r[v]. Время прибытия t[v] можно незамедлительно уменьшить до d[v]. Это позволяет уточнить вторую команду:
[math]\displaystyle{ \neg P3 \and P2 \and \exist v \in V: t[v] = max(t) \to r[v], t[v] :=r[v] + 1, d[v] \; }[/math].
Поскольку во время выполнения этой операции регистры перемещаются, предикат P2 может перестать выполняться. Однако первая команда восстановит статус кво. Эта команда увеличивает t для некоторых вершин; некоторые из них даже могут превысить значение max(t) до перемещения регистра. Аналогичное рассуждение для [math]\displaystyle{ \langle r, t \rangle \; }[/math] показывает, что их значения r также подвергаются увеличению. Таким образом, для реализации данного «насколько возможно быстрого» (As-Soon-As-Possible, ASAP) увеличения r необходимо сделать моментальный снимок max(t), пока предикат P2 еще актуален. Физически такой моментальный снимок записывает один такт применимой длительности [math]\displaystyle{ \phi \; }[/math] и может быть реализован при помощи добавления к циклу еще одной команды:
[math]\displaystyle{ P2 \and \phi \gt max(t) \to \phi := max(t) \; }[/math].
Однако подобная ASAP-операция может увеличить r[u] даже в случае w[u, v] - r[u] + r[v] = 0 для ребра (u, v). Это означает, что P0 может быть уже не инвариантом. Однако перемещение P0 из инварианта в цель цикла не составит проблемы, поскольку для этого в цикл можно добавить одну команду:
[math]\displaystyle{ \exist (u, v) \in E: r[u] - r[v] \gt w[u, v] \to r[v] := r[u] - w[u, v] \; }[/math].
После объединения всех нововведений алгоритм приобретает следующую форму.
[math]\displaystyle{ r, t, \phi := 0, d, \infty \; }[/math] do {P1} [math]\displaystyle{ \exist \; (u, v) \in E: r[u] - r[v] = w[u, v] }[/math] [math]\displaystyle{ \and \; t[v] - t[u] \lt d[v] \to t[v] := t[u] + d[v] }[/math] [math]\displaystyle{ \neg P3 \and \exist \; v \in V: t[v] \ge \phi }[/math] [math]\displaystyle{ \to r[v], t[v] := r[v] + 1, d[v] }[/math] [math]\displaystyle{ P0 \and P2 \and \phi \gt max(t) \to \phi := max(t) }[/math] [math]\displaystyle{ \exist \; (u, v) \in E: r[u] - r[v] \gt w[u, v] }[/math] [math]\displaystyle{ \to r[v] := r[u] - w[u, v] }[/math] [math]\displaystyle{ od \{ P0 \and P1 \and P2 \and P3 \}. \; }[/math]
Название | Кол-во | Длительность такта | [math]\displaystyle{ \sum r }[/math] | Кол-во | Время | ASTRA | ||
---|---|---|---|---|---|---|---|---|
вентилей | до | после | обновлений | A(s) | B(s) | |||
s1423 | 490 | 166 | 127 | 808 | 7619 | 0,02 | 0,03 | 0,02 |
s1494 | 558 | 89 | 88 | 628 | 7765 | 0,02 | 0,01 | 0,01 |
s9234 | 2027 | 89 | 81 | 2215 | 76943 | 0,12 | 0,11 | 0,09 |
s9234.1 | 2027 | 89 | 81 | 2164 | 77644 | 0,16 | 0,11 | 0,10 |
s13207 | 2573 | 143 | 82 | 4086 | 28395 | 0,12 | 0,38 | 0,12 |
s15850 | 3448 | 186 | 77 | 12038 | 99314 | 0,36 | 0,43 | 0,17 |
s35932 | 12204 | 109 | 100 | 16373 | 108459 | 0,28 | 0,24 | 0,65 |
s38417 | 8709 | 110 | 56 | 9834 | 155489 | 0,58 | 0,89 | 0,64 |
s38584 | 11448 | 191 | 163 | 19692 | 155637 | 0,41 | 0,50 | 0,67 |
s38584.1 | 11448 | 191 | 183 | 9416 | 114940 | 0,48 | 0,55 | 0,78 |
Таблица 1. Экспериментальные результаты
Для завершения разработки алгоритма осталось реализовать проверку [math]\displaystyle{ \neg P3 }[/math]. Из предыдущего обсуждения мы уже знаем, что из [math]\displaystyle{ \neg P3 }[/math] следует, что существует такая вершина u, что [math]\displaystyle{ r[u] - r'[u] \ge r[v] - r'[v] \; }[/math] после каждого увеличения r[v]. Это означает, что [math]\displaystyle{ max_{v \in V} \; r[v] - r'[v] }[/math] не будет увеличиваться. Иначе говоря, существует по меньшей мере одна вершина v, у которой r[v] не будет меняться. До увеличения r[v] имеет место соотношение [math]\displaystyle{ w_{u \rightsquigarrow v} - r[u] + r[v] \le 0 \; }[/math], где [math]\displaystyle{ w_{u \rightsquigarrow v} \ge 0 \; }[/math] – исходное количество регистров на одном пути из u в v, в результате чего неравенство [math]\displaystyle{ r[v] - r[u] \le 1 \; }[/math] остается верным даже после увеличения r[v]. Из этого следует, что будет по меньшей мере i + 1 вершин, у которых r не превышает i для [math]\displaystyle{ 0 \le i \lt |V| \; }[/math]. Иными словами, алгоритм может по-прежнему увеличивать r, и когда какое-либо значение r достигнет |V|, это покажет, что условие P3 удовлетворяется. Таким образом, полный алгоритм имеет следующую форму:
[math]\displaystyle{ r, t, \phi := 0, d, \infty \; }[/math] do {P1} [math]\displaystyle{ \exist \; (u, v) \in E: r[u] - r[v] = w[u, v] }[/math] [math]\displaystyle{ \and \; t[v] - t[u] \lt d[v] \to t[v] := t[u] + d[v] }[/math] [math]\displaystyle{ (\forall \; v \in V: r[v] \lt |V|) }[/math] [math]\displaystyle{ \and \; \exist \; v \in V: t[v] \ge \phi \to r[v], t[v] := r[v] + 1, d[v] }[/math] [math]\displaystyle{ (\exist \; v \in V: r[v] \ge |V|) }[/math] [math]\displaystyle{ \and \; \exist \; v \in V: t[v] \ge \phi \to r[v], t[v] := r[v] + 1, d[v] }[/math] [math]\displaystyle{ P0 \and P2 \and \phi \gt max(t) \to \phi := max(t) }[/math] [math]\displaystyle{ \exist \; (u, v) \in E: r[u] - r[v] \gt w[u, v] }[/math] [math]\displaystyle{ \to r[v] := r[u] - w[u, v] }[/math] [math]\displaystyle{ od \{ P0 \and P1 \and P2 \and P3 \} \; }[/math].
Корректность алгоритма можно легко показать в силу того, что P1 остается инвариантом и из отрицания предикатов следует [math]\displaystyle{ P0 \and P2 \and P3 \; }[/math]. Завершение работы алгоритма гарантируется монотонным возрастанием r и его верхней границей. Следующая теорема задает время выполнения в наихудшем случае.
Теорема 1. Время выполнения данного алгоритма ресинхронизации в наихудшем случае ограничено сверху значением [math]\displaystyle{ O(|V|^2 \; |E|) }[/math].
Время выполнения алгоритма ресинхронизации в наихудшем случае будет актуальным в случае, когда каждое увеличение r приводит к «протягиванию» синхронизации по всей схеме (т.е. по |E| ребрам). Это верно только тогда, когда увеличение r перемещает все регистры в схеме. Однако в таком случае верхняя граница r равна 1, и время выполнения не превышает O(|V| |E|). С другой стороны, если значение r велико, схема разбивается регистрами на несколько меньших фрагментов, в результате чего протягивание, вызванное увеличением одного r, ограничено деревом небольшого размера.
Применение
В базовом алгоритме оптимальность P3 проверяется условием [math]\displaystyle{ r[v] \ge |V| \; }[/math]. Однако в большинстве случаев условие оптимальности можно обнаружить намного раньше. Поскольку при каждом возрастании r[v] должна существовать «вершина-хранитель» u, такая, что после выполнения действия будет верно неравенство [math]\displaystyle{ r[u] - r'[u] \ge r[v] - r'[v] \; }[/math]. Следовательно, если ввести указатель из v на u при увеличении r[v], указатели не смогут образовать цикл согласно [math]\displaystyle{ \neg P3 }[/math]. Фактически указатели образуют лес, в котором корни имеют значение r = 0, а потомок может иметь значение r, не более чем на 1 превышающее значение его предка. Использование цикла указателей как свидетельство верности P3 вместо [math]\displaystyle{ r[v] \ge |V| \; }[/math], можно значительно повысить практическую эффективность алгоритма.
Открытые вопросы
Ресинхронизация обычно используется для оптимизации длительности цикла либо количества регистров в схеме. Описанный алгоритм решает только задачу ресинхронизации с достижением минимальной длительности. Задачу ресинхронизации с достижением минимального количества регистров для заданной длительности цикла решили Лейзерсон и Сакс [1], она представлена в соответствующей статье. Их алгоритм сводит задачу к двойственной проблеме поиска сетевого потока с минимальной стоимостью в плотном графе. Остается открытым любопытный вопрос – можно ли разработать эффективный итеративный алгоритм для решения задачи о минимальном количестве регистров, схожий с алгоритмом Чжоу.
Экспериментальные результаты
Результаты были опубликованы Чжоу [3] по итогам сравнения времени выполнения алгоритма с эффективной эвристикой под названием ASTRA [2]. Результаты прогона на эталонных тестах ISCAS89 представлены в таблице 1 из работы [3]; столбцы A и B таблицы отражают время выполнения двух этапов ASTRA.
См. также
Литература
1. Leiserson, C.E., Saxe, J.B.: Retiming synchronous circuitry. Algorithmica6,5-35(1991)
2. Sapatnekar, S.S., Deokar, R.B.: Utilizing the retiming-skew equivalence in a practical algorithm for retiming large circuits. IEEE Transactions on Computer Aided Design 15,1237-1248 (1996)
3. Zhou, H.: Deriving a new efficient algorithm for min-period retiming. In: Asia and South Pacific Design Automation Conference, Shanghai, China, January 2005