В викенд я зашел в кафе Red Rock и встретил там программистку встроенных систем Машу Горбунову. Вообще, у этого кафе в Маунтин-Вью, Калифорния можно встретить кого угодно - например однажды на меня прямо из-за угла вылетел основатель Гугла Сергей Брин. Так вот Мария рассказала мне что программирует RTOS (семафоры, мейлбоксы, сигналы), чему выучилась в свое время в питерском институте ГУАП (аэрокосмического приборостроения).
Я решил, что такая девушка не должна оставаться в другой отрасли и показал ей плату ПЛИС, внутри которого можно засинтезировать пару ядер ARM микроконтроллерного класса. На что Маша среагировала так:
Как процессор можно засунуть в ПЛИС? Очень просто. ПЛИС - это матрица ячеек, логическую функцию которых можно менять извне. Главным элементом ячейки является LUT - LookUp Table. LUT можно превращать в И, ИЛИ, ИСКЛЮЧАЮЩЕЕ-ИЛИ (XOR) и другие, просто меняя четыре входа конфигурации, которые определяют 16 логических функций. Два других входа - рабочие, аргументы X0 и X1, а выход Y - результат. Он в зависимости от конфигурации abcd, у может работать как y = x0 & x1 или y = x0 | x1, или y = ~ x0 & x1 итд:
Кроме комбинационной логики, в ячейках ПЛИС есть D-триггеры, минимальные элементы памяти/состояния, из которых можно строить конечные автоматы и конвейеры.
Так как для Маши D-триггеры и LUT-ы сами по себе были недостаточно убедительны (у них в RTOS-а тоже есть свои хитрости), я показал Маше мероприятие в Грузии под названием lalambda.school. Вообще оно посвящено формальным методам, но в этом году мы с разработчиком ПЛИСов Дмитрием Смеховым собрались показывать там и ПЛИСы.
Мероприятие LaLamba понравилось Маше больше - костюмы и тусование как на Burning Man, но только не в пустыне, а в отеле и под программирование с математикой: Coq, OCaml, Lisp, Haskell, Purescript, SAT солверы и вот теперь и верилог:
Coq - это система автоматического доказательства теорем. Например на нем можно написать выражения с кванторами всеобщности и существования, скажем:
Что означает "для всех X и Y, из того, что X*Y=0 следует, что или X=0, или Y=0". И система Coq может это все доказывать, а если утверждение неверно, то находить к этому контрпримеры.
Какое это все имеет отношение к проектированию железа? В железе тоже используются системы автоматического доказательства. Есть попроще - проверки эквивалентности утверждений комбинационной логики, а есть посложнее - доказательство утверждений так называемой темпоральной логики.
Пример утверждения темпоральной логики на языке описания аппаратуры SystemVerilog:
Оно означает "если в начале такта сигнал valid был активен, а сигнал ready - нет, то в начале следующего такта сигнал valid должен все еще стоять". Программы автоматического доказательства свойств цифровой схемы, например стоящий бешеные деньги Cadence Jasper Gold, умеют применять формальные методы для доказательства подобных утверждений. Или находить контрпримеры к этим утверждениям для данной схемы и показывать их на временных диаграммах:
Можно ли делать доказательства утверждений темпоральной логики с помощью Coq или open-source тулов? Я как-раз и собираюсь выяснить это на тусовке, где будет много специалистов по такого рода тулам.
У меня к ним много и других вопросов, например можно ли с помощью Haskell делать constraint solver-ы для генерации псевдослучайных транзакций с отношениями, заданными между полями объекта? Коммерческие тулы, которые это делают (Synopsys VCS, Cadence Xelium, Siemens EDA Questa) тоже весьма платные, хотя есть какая-то бесплатная версия в Xilinx Vivado.
Я принес Маше книжки и на эту тему, по SystemVerilog Assertions (утверждениям темпоральной логике) и верификации цифровых схем на уровне регистровых передач. Так как это способ для хорошей програмистки, особенно которая сечет в RTOS, перейти в хардвер (сначала в верификацию, а потом в дизайн).
По этому поводу я даже написал документ, правда на английском языке, по запросу от Дениса Лобзова из Siemens EDA, который продвигает идею внедрить верификацию аппаратных блоков в систему высшего образования Армении. Вот он - можете покритиковать.
Если кратко и по-русски, то инженер-верификатор аппаратных блоков - это:
Хороший программист, может писать умные тестовые окружения с проверкой схемы против модели на уровне транзакций. C очередями и таблицами текущих транзакций и их состояний, параллельными процессами, почтовыми ящиками, сигналами, семафорами итд.
Понимает основы проектирования на уровне регистровых передач (Register Transfer Level - RTL): комбинационную и последовательностную логику, D-триггеры, конвейеры, тактовые домены и протоколы шин систем на кристалле типа AXI.
Владеет специфическими методами верификации: автоматическое определение покрытия интересных сценариев (functional coverage), constraint solver для ограниченно-случайных транзакций, доказательства выражений темпоральной логики.
Организацию ликбеза по основам проектирования на уровне регистровых передач мы уже обсуждали с другой Машей, Машей Горчичко, которая училась в МИФИ (институте с ядерным реактором внутри), а сейчас работает исследователем в Applied Materials (оборудование для производства передовых нанометров). Маша в свое время была помощником преподавателя на лабах по ПЛИС в Университете Вандербильда в Теннесси. Я ее тоже собираюсь сагитировать прилететь на мероприятие в Тбилиси (нельзя же все время работать):
Основы синтеза схем на уровне RTL можно начинать и с еще более простых упражнений, с кнопочками и лампочками, причем от них можно перейти ко вполне взрослым упражнениям с арбитрами. О таком часто спрашивают на интервью в электронные компании - "напишите арбитр". Вот как это выглядит на минималистической плате (код):
После изучения концепций счетчиков и конечных автоматов необязательно сразу нырять в конструирование процессоров (хотя и это будет). Можно также заняться распознаванием и генерацией звука чистым хардвером ПЛИС, без процессора и софтвера:
Сначала определять ноту с помощью аппаратного счетчика, который считает, сколько тактов 50-мегагерцового тактового сигнала прошло между пересечениями некоего порога уровнем сигнала с микрофона.
Затем сделать параллельно работающие конечные автоматы для определения мелодий.
Мы могли бы распознавать звуки от генератора частоты в смартфоне, но это неспортивно. За живые мелодии во время семинара отвечает преподавательница флейты Маша Беличенко. Она же, в качестве арт-программы, обучает участников играть простые мелодии на блокфлейте. Маша привезет пару десятков блокфлейт, так что должно хватить для всех участников семинара с ПЛИСами.
Такого рода упражнения не требуют знания математики DSP (цифровые фильтры, преобразование Фурье). Но в конце всего мероприятия будет хакатон, на котором можно попробовать и DSP, для всяких музыкальных эффектов. Благо вокруг будет много товарищей, которые еще не забыли матан.
Для начальной подготовки к упражнениям с верилогом и ПЛИС я рекомендую почитать в самолете на пути в Грузию книжку "Цифровая схемотехника и архитектура компьютера", которую держит в руке Маша Хохлова, выпускница Физфака МГУ, которая сейчас занимается беспилотниками. Бесплатный русский перевод этой книжки (версию для MIPS 2012 года) можно скачать здесь, а более новую версию 2022 года (с архитектурой RISC-V) можно найти в Доме Книги на Новом Арбате в Москве или на сайте ДМК-Пресс. С ней хорошо идет лабник "Цифровой Синтез".
Я разумеется попробую уговорить Машу с беспилотниками приехать в Тбилиси, точно так же как и Машу-блондинку, Машу-рыжую и Машу-флейтистку. Еще есть Маша-математик из Интела, которую я однажды случайно встретил в московском метро (она занималась конечными автоматами, так что ей грех не приехать на верификацию их формальными методами), а также две Маши, которые уже записались на слет в Тбилиси - одна пишет на языке Rust, а другая на питоне и читает иероглифы. Приезжайте и вы