Начиная с января 2012 занимаюсь синтезом hardware из LTL спецификаций в
TU Graz.
На вход принимается описание схемы в виде linear temporal logic (
LTL). LTL содержит стандартные логические операторы
and/or/not и временные операторы
Globally/Future/Until. Благодаря этому можно описывать "временные" свойства системы. Например, формула
G(r -> Fg)описывает простой арбитер и означает "
Gлобально(в любой момент времени), если наблюдаем на входе сигнал r(request), то в будущем (in the
Future), необходимо поднять сигнал g(grant)".
Из этой спецификации синтезируется автомат Мура (можно и Мили).
В кратце, это и есть проблема
синтеза реактивной системы. Реактивная система - не очень хорошее название, более правильно сказать реагирующая система, система, которая постоянно находится во взаимодействии с окружением и никогда не останавливается. Это отличает её от "data crunch" систем, которые поглощают input data, обрабатывают её , выдают ответ и останавливаются. Примером реактивной системы может быть сотовый телефон, банкомат, сосед по парте.
Формально проблема синтеза выглядит так:
вход: LTL спецификация, разделение переменных на input/output
выход: автомат, либо "нет", если спецификация противоречивая
Проблема не новая. Первые работы - в 60х годах. Например, вот эта работа цитируется практически всеми -
On the synthesis of a reactive module (1989). Сложность однако заключается в нижней вычислительной сложности синтеза - 2EXPTIME (double exponential) относительно размера спецификации. Как результат - малопрактично и мало внимания уделялось. Исследователи подходили с разных сторон к облегчению проблемы - ограничивали язык спецификации, например (
GR1 synthesis). Другой подход - это ограничить вид синтезируемых автоматов. Например, можно рассматривать только автоматы малого размера. Это важно с практической точки зрения - инженеров может не интересовать автомат, который хотя и отвечает спецификации, зато имеет 10000 состояний.
Где то в 2005 году и началось второе рождение этой области. Ключевая статья -
Safraless decision procedures.
Сейчас мы используем для синтеза
bounded synthesis метод, который позволяет задать лимит на размер синтезируемого автомата. Внутри, метод сначала конвертирует LTL спецификацию в Universal coBuchi Automaton, затем в
SMT query, который отправляется в SMT solver Z3 (по сути, проблема синтеза конвертируется в проблему SAT).
Мы сейчас работаем над близкой, но несколько иной проблемой - проблемой параметризованного синтеза (
Parameterized Synthesis). Проблема совсем новая.
Проблема параметризованного синтеза выросла естественно из обычного синтеза. Схемы, которые пытались и пытаются синтезировать часто представляют собой разного рода арбитры, контроллеры, которые контроллируют доступ клиентов к некому ресурсу. Например,
AMBA bus arbiter. Спецификация этого арбитра описывает доступ к общей шине нескольких клиентов. Клиент может запросить доступ к шине, получить доступ, переслать данные по шине, освободить шину, итд. Необходимо уметь синтезировать подобный арбитр. Но для скольких клиентов? Можно синтезировать разные арбитры для 2-3-4.. клиентов. Но возникает проблема - чем больше клиентов, тем сложнее задача.
На картинке вверху - время синтеза простого и посложнее арбитров в зависимости от числа клиентов. Зеленая штриховая линия - это время которое понадобилось бы, если бы не следующая идея.
Идея параметризованного синтеза простая - можно ли синтезировать базовый блок, который можно размножать и соединять друг с другом, масштабируя систему? Для некоторых спецификаций это можно. Например, это работает для простого арбитра со следующей спецификацией:
forall(i) G(r_i -> Fg_i)
forall(i != j) G(! (g_i & g_j))
Т.е. каждый request в конечном итоге обслужен, но невозможно одновременное предоставление гранта двум клиентам. Здесь, не задано конкретное число клиентов.
Для решения проблемы параметризованного синтеза мы используем интересный "
cut-off" результат. Если рассматривать блоки организованные в token-rings, то для некоторых видов спецификаций достаточно синтезировать token-ring размера 4. Если удается синтезировать token ring такого размера, то из него можно вытащить базовый блок. Базовый блок затем можно соединять в token-rings любого размера.
Будущие направления:
- применить другие cut-off результаты
- cut-off independence: проверять, возможно ли масштабирование синтезированной схемы для случаев, для которых нет cut-off результатов
- ускорять синтез - процесс страшно медленный (сейчас удается синтезировать базовый блок из 4ех состояний за разумное время, этого мало)
Пара ссылок:
презентация на alpine verification meeting
основная статья, в которой была представлена проблема -
Parameterized Synthesis
