Политкорректность проникает в Россию через книги про проектирование чипов на SystemVerilog для не-начинающих

Первое слово в книжке после предисловий — «симулятор». Для понимания языков описания аппаратуры нужно четко отдавать себе отчет, что синтезируемое подмножество верилога — это не язык программирования, а язык описания электрических схем. Так же как скажем HTML — не язык программирования, а язык описания веб-страниц. В то время как язык программирования предназначен для компиляции в цепочку команд процессора, язык описания аппаратуры предназначен для превращения (в частности) в железо процессора как такового. При этом до отлития в железо код на языке описания аппаратуры нужно проверить, для чего служит специализированный интерпретатор, называемый симулятором.

В начале книги Дональд Томас показывает упрощенную картинку симулятора, а в конце книги ее уточняет и дополняет:

В симуляторе есть очереди событий и симулируемое время:

Событие может породить новое событие, как в текущий момент симуляции (в текущем дельта-цикле), так и в будущем времени. В текущем дельта-цикле сначала обрабатываются все события, порождаемые так называемыми блокирующими присваиваниями, а потом — события, порождаемые неблокирующими присваиваниями. Это необходимо для корректного моделирования параллельной семантики распостранения электрических сигналов в железе:

Кроме синтезируемого подмножества верилога есть еще несинтезируемое подмножество. Оно предназначено для описания тестового окружения и тестов, и вот его можно рассматривать как своего рода язык программирования. Для событий тестового окружения и мониторов вводятся дополнительные шаги симулятора:

Точное знание алгоритма работы симулятора очень полезно, чтобы избежать разнообразных багов, связанных с так называемыми гонками (race condition). Когда я интервьирую инженеров, я всегда прошу их привести пример race condition в языке Verilog. Причем если для юных RTL Design и Design Verification Engineers такое знание очень желательно, но не во всех аспектах 100% обязательно, то есть профессии, в которых за это знание платят деньги непосредственно. Я говорю о программистах, которые работают в командах Synopsys VCS, Cadence IES и Mentor ModelSim.

Synopsys и Cadence — это две компании, которые находятся в Калифорнии в 15 минутах езды друг от друга. В них работает всего несколько тысяч человек, но они контролируют разработку микросхем во всем мире — в Intel, Apple, Samsung, Huawei, даже в секретных российских институтах, которые делают чипы для военной техники.

Если товарищи Путин, Рогозин и Вексельберг реально хотят ввести в России импортозамещение, то они могли бы сфинансировать разработку российского аналога Synopsys VCS (для симуляции верилога), Synopsys Design Compiler (для логического синтеза верилога) и Synopsys IC Compiler (для физического размещения результатов логического синтеза). Вероятно несколько тысяч математически-подкованных программистов в России найдется.

Хотя лицензии на эти программные продукты довольно легко ломать, но использовать их без суппорта тяжело. Если Huawei отключат от Synopsys и Cadence, им придется в некотором смысле хуже, чем при отключении от Android-а и даже ядер ARM.

Да, так вот уточненный алгоритм в конце книжки Дональда Томаса. Если вы не выучите его назубок, интервьироваться в группы симуляции в Synopsys, Cadence, Siemens/Mentor, Xilinx итд бесполезно — там от вас попросят нарисовать это на доске и предложат придумать, как оптимизировать какой-нибудь частный случай:

После прояснения с симуляцией в начале книжки Дональд Томас описывает язык SystemVerilog как таковой. Этот язык возник как суперсет Verilog-а в 2002 году, в результате слияния языков Verilog-2001, Vera и Superlog, и с добавлениями идей от Property Specification Language (PSL), которые трансформировались в SystemVerilog Assertions (SVA).

Дональд Томас считает, что вы уже где-то выучили основы цифрового проектирования, поэтому вплетает в ткань повествования разные известные штуки типа карт Карно. Карты Карно использовали для ручного проектирования схем в 1960-е годы, после чего этот метод заменили автоматической оптимизацией логики с помощью алгоритма Куайна — Мак-Класки и автоматическим оптимизатором логики Espresso. Поэтому карты Карно присутствуют во всех вузовских учебниках по проектированию цифровой логики, но как бы висят в воздухе. И вот Дональд Томас привязывает карты Карно к жизни проектировщика на верилоге 21-го века:

Далее Дональд Томас пишет про конечные автоматы, причем приводит 1) строгое математическое определение; 2) диаграммы; 3) код; 4) после чего начинает их расширять до конечных автоматов с трактом данных — аппаратных потоков; 5) после чего эти потоки начинают у него взаимодействовать, как по простым «политкорректным» (см. выше) протоколам, так и с помощью аппаратных очередей.

Вот код простого автомата с трактом данных, которые Томас приводит в качестве первого примера:

Далее у Томаса идет глава про статический анализ тайминга. Ничего особого, но чище, чем на многих популярных индийских сайтах «Как пройти VLSI интервью». А также более полно, чем в некоторых книгах по верилогу, которые нудно разжевывают синтаксис языка, но не очень показывают, как его использовать.

Зачем нужен статический анализ тайминга? В реальном железе, в отличие от иллюзии, которую процессор показывает программисту, каждое вычисление проходит через временной интервал, когда на проводах находится всякий мусор — не только четко вычисленные нули и единицы, но и всякие случайные глюки, то бишь glitch-и, и вообще не-цифровые значения в запрещенном интервале (forbidden zone). Например если у вас все напряжения выше 0.7 вольт считаются цифровой единицей, а все напряжения ниже 0.3 вольт — цифровым нулем, то на проводе может оказаться 0.4 вольта.

В конце концов все сигналы в схеме проходят свой путь и ситуация устаканивается, но это «в конце концов» должно быть меньше цикла тактового сигнала (clock). Этот цикл обратно пропорционален частоте, на которой работает схема (гигагерцы, мегагерцы).

Если устаканившийся результат вычислений или логических операций не попадет в D-триггер (минимальный элемент памяти) в момент апертуры (интервал вокруг изменения такового сигнала), состояние схемы станет мусорным — спутник или реактор взорвется, айфон перестанет отвечать на звонки. Всю эту тему проектировшику аппаратуры нужно знать не менее железно, чем логику.

Почему анализ статический? В 1980-е годы он был динамический — задержки выясняли с помощью симуляции. Это оказалось ненадежным для схем с сотнями тысяч, миллионами и миллиардами транзисторов, и теперь все задержки рассчитывают статически, на основе анализа путей сигналов после синтеза.

Тактовый сигнал тоже может приходить в разные части микросхемы с некоторое задержкой, что добавляет к этой кухне еще одну неопределенность, от которой нужно избавляться (к счастью не вручную, а с помощью программ синтеза дерева тактовых сигналов и других методов):

В главе про потоки Томас разбирает несколько базовых вариантов, как параллельно работающие конечные автоматы с трактами данных могут обмениваться информацией, в том числе используя буфера и очереди. Как в самом дизайне / схеме ну уровне регистровых передач, так и в поведенческой модели или тестовом окружении схемы. При чтении Томаса неплохо самому написать и отладить примеры для всех случаев описанных им протоколов. Дело в том, что код на такие темы (небольшой контролирущий конечный автомат, поток данных между двумя модулями, конвейерные тракты данных или просто код для аппаратной очереди) любят давать писать на доске или на компьютере во время интервью второго уровня в электронных компаниях. Если вы можете написать пример для любой из описанных у Томаса комбинаций за 20 минут с кодом на 30-50 строк, то вы произведете хорошее впечатление. Тяжело в учении — легко в бою.

Тестовое окружение для роутеров (рис. 8.3) с очередями для нескольких портов — это популярный пример, который используют для объяснения методологий верификации. Наверное потому что некоторые из этих методологий изобрели в Cisco и других компаниях, проектирующих чипы для сетевого хардвера.

В главе 6.2.2. Томас описывает один из вариантов взаимодействия потоков — пошаговую синхронизацию (Lock-step). Одно из применений lock-step — системы высокой надежности, например в автомобильной электронике. Частный случай: два процессора могут исполнять одну и ту же программу с задержкой в несколько циклов, и в процессе этого выполнения специальная схема может проверять, что у них совпадают результаты.

Томас явно занимался надежностью, так как помимо lock-step он приводит использование CRC, циклически избыточный код для обнаружения ошибок при передаче данных. При этом Томас рассказывает, как вычислить CRC с помощью LFSR — регистр сдвига с линейной обратной связью. И то, и другое нужно уметь молодому инженеру. В этом достоинство книжки Томаса — хотя она не всегда копает глубоко, она касается многих тем и показывает где надо копать:

При описании CRC Томас ссылается на очень занятную и неправильно понятую в России книжку Hacker’s Delight:

Дональд Томас в своей новой книжке затрагивает и три технологии, которых вообще не было в старой книжке:

1. Автоматическую генерацию псевдослучайных транзакций с правилами ограничений (constrained random transactions / constraint solvers).
2. Учет покрытия возникающих при бомбардировке дизайна ограниченно-случайными транзакциями интересных сценариев, функциональное покрытие (functional coverage).
3. Язык утверждений темпоральной логики (concurrent assertions) и использование его как при симуляции, так и при автоматическом доказательстве свойств дизайна с помощью программ формальной верификации.

Эти три технологии вошли в индустрию по хорошему только в XXI веке, но зато вошли довольно крепко. Сначала они все применялись при создании сред тестирования верификационными инженерами, но сейчас знание функционального покрытия и языка темпоральных утверждений (SystemVerilog Assertions — SVA) требуют и от дизайнеров. У Томаса приведен некий минимум, который поможет вам не зарубиться на скажем телефонном интервью, но для реальной работы вам нужно знать гораздо больше. Причем не только язык темпоральных утверждений как таковой, но и практику отладки с его помощи порождаемых симулятором параллельных конечных автоматов для каждого утверждения, а также использования программ формальной верификации. Assertion-based formal verification в последние годы сильно внедрили внутри Apple, AMD и других таких компаний.

У меня есть приятель, который скачал вот такую книжку по языку темпоральных утверждений и изучал ее все новогодние каникулы вместо поездки на Гавайи с девушками. Отсюда вы можете понять насколько SystemVerilog Assertions (SVA) важны для карьеры и индустрии. Правда для полноты картины я должен упомянуть, что он сын эмигрантов из Тайваня, и у них более суровое отношение к таким вещам, чем у русских.

Вот как Томас касается генерации псевдослучайных транзакций (транзакция с полями rand и их ограничение с помощью конструкции constraint):

А вот как Томас касается functional coverage — covergroup/coverpoint/bins, учет комбинаций покрытий нескольких переменных (cross), использование wildcard bins, диапазоны значений, а также покрытия переходов в конечных автоматах:

Вот пример простейшего темпорального утверждения «если на позитивном фронте тактового сигнала q истинно, то через цикл должна выполнится последовательность s2, в которой сначала истинно r, а еще через три цикла — s»: