Наконец-то в России вышел учебник по SystemVerilog уровнем выше чем для начинающих. Учебник описывает технологии и приемы, которые спрашивают на интервью в NVidia, Intel, AMD, Apple и другие электронные компании: использование concurrent assertions и functional coverage, что сейчас требуют не только от инженеров по верификации, но и от дизайнеров микросхем; алгоритм работы симулятора с дельта-циклами; вменяемое объяснение static timing analysis; схемы коммуникации аппаратных блоков через аппаратные очереди; реализацию этих коммуникаций с помощью конечных автоматов с трактами данных и т.д.
В главе про последнее российского читателя может озадачить упоминание «политкорректной системы». Что бы это значило? Это вероятно намек на казус, который произошел в округе Лос-Анжелес в 2003 году. Чиновники Лос-Анджелеса попросили производителей, поставщиков и подрядчиков прекратить использование терминов «master/slave» («хозяин» и «раб») в отношении компьютерного оборудования, так как одному из работников округа эти термины напомнили про рабовладельческое прошлое.
Сейчас авторы технической литературы избегают терминов master/slave. В современной Америке работают и афро-американские инженеры (например София Мвокани из Камеруна — на фото слева), и использование старых терминов выглядит архаично, как выглядели бы например термины «пан/холоп» в украинской технической литературе вместо принятых «провідний/ведений» (рус. «ведущий/ведомый»).
Это не первый раз, когда в российском электронном образовании появляется тема борьбы афро-американцев за гражданские права. Например Татьяна Волкова, известный специалист по образованию в электронике, носит маечку с эмблемой «Черных Пантер», калифорнийского движения, которое в свое время сочло мирный протест недостаточным, и занялось вооруженным протестом.
Полное изображение эмблемы под кожанкой Татьяны Александровны — под катом, но в основном я буду рассказывать про дельта-циклы и конечные автоматы:
Ниже скриншот статьи про master / slave и обещанная эмблема «Черных пантер», после чего мы переходим к книжке как таковой.
Прежде всего, Дональд Томас, автор книги «Логическое проектирование и верификация систем на SystemVerilog» (2019 год на русском языке от ДМК-Пресс, 2016 год на английском) — это тот же самый Дональд Томас, который в соавторстве с Филиппом Мурби написал книжку 1991 года «The Verilog Hardware Description Language» by Donald Thomas and Philip Moorby. Тогда, в 1991 году, многие электронные компании еще проектировали микросхемы по старинке, рисуя их мышкой на экране; технологии логического синтеза только-только вышли из лаборатории на производство; языки описания аппаратуры считались предназначенными для написания моделей и тестов, а не исходниками для создания окончательных схем; помимо VHDL и закрытого в то время Verilog-а было много мелких и проприетарных языков типа Abel, CUPL, PALASM; а у Intel и MIPS были внутренние языки описания аппаратуры.
Вот в такой обстановке вышла книжка Томаса и Мурби, которая стала для проектировщиков цифровых микросхем 1990-х тем же, чем для программистов на Си стала книжка Керниган-Ричи, а для программистов на C++ — книги Бьярни Страуструпа. Книжка выдержала пять изданий — от 1991 года до 2002, но для эпохи Айфонов была явно недостаточна. И вот в 2016 году Дональд Томас решил наверстать и выпустил новую книжку, в которой описал ключевые нововведения в язык и методологии за 25 лет. Те самые 25 лет, в течение которых Verilog стал общей базой для всей индустрии, на нем пишутся схемы для всего — от пресловутых айфонов и контролирующих компьютеров в Теслах до российских военных вертолетов.
Далее я буду выделять свои комментарии синим текстом, чтобы отделить их от картинок из книги.
Еще перед основным текстом книги поставлена пред-глава «Контекст: проектирование на уровне регистровых передач», чтобы случайно взявший с полки эту книжку программист, школьник или скажем любитель упражняться с макетными платами сразу поняли, о чем идет речь и как они могу применить книжку. В ней говорится:
Сейчас производятся цифровые системы с миллиардами транзисторов на кристалле. Любитель, конечно, может в качестве спецификации (для реализации на макетной плате) нарисовать несколько логических вентилей и соединить их проводами, но для коммерческих проектов это древняя история.… Современные системы специфицируются на языках описания аппаратуры, таких как 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:
Дональд Томас в своей новой книжке затрагивает и три технологии, которых вообще не было в старой книжке:
- Автоматическую генерацию псевдослучайных транзакций с правилами ограничений (constrained random transactions / constraint solvers).
- Учет покрытия возникающих при бомбардировке дизайна ограниченно-случайными транзакциями интересных сценариев, функциональное покрытие (functional coverage).
- Язык утверждений темпоральной логики (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»:
Что читать перед и после книги «Логическое проектирование и верификация систем на SystemVerilog» Дональда Томаса?
Если вы не поняли вообще ничего в моем посте, то вы можете попробовать почитать книжку “Цифровая схемотехника и архитектура компьютера” Дэвида Харриса и Сары Харрис. Книжку Харрис & Харрис могут понять все, кто умеет читать и считать, при условии, что у читателя есть мотивация. Книжка начинается с уровня средней школы — напряжений, двоичных чисел — и заканчивается проектированием собственного процессора на верилоге.
Спойлер: Дэвид Харрис и Сара Харрис не муж и жена и даже не брат и сестра. Они просто однофамильцы, которые случайно стали работать преподавателями в одном и том же университете, в процессе чего написали книжку.
Вот слева на фотографии девушка Ирина из новосибирского Академгородка держит английское издание Харрис & Харрис, а справа — ее русское издание.
dmkpress.com/catalog/electronics/circuit_design/978-5-97060-522-6
После книжки Дональда Томаса я рекомендую скачать статьи Клиффа Каммингса. Он самый известный тренер по верилогу как для синтеза, так и для верификации. При чтении книги Дональда Томаса у меня много раз возникала мысль «а вот тут хорошо бы вставить для полноты такой-то кусок из Клиффа Каммингса». Клифф берет на семинарах по $1000-$3000 за каждого слушателя, в зависимости от продолжительности семинара (от дня до недели), и электронные компании платят, чтобы повысить качество своих инженеров, недостаточно выученных в вузах. Даже в Стенфорде увы, не все это учат — у меня был интерн из Стенфорда, от него я это знаю. Если вы скачаете все бесплатные статьи Клиффа Каммингса после чтения Дональда Томаса, то вы сэкономите все эти деньги.
Вот эти две статьи обязательны — это любят спрашивать везде на интервью:
Clock Domain Crossing (CDC) Design & Verification Techniques Using SystemVerilog
Вот эти две статьи прочитать желательно, особенно про снятие асинхронного ресета, перекодирование состояний FSM и cтиль FSM «case (1'b1) // synopsys parallel_case», который давно использовался в высокоскоростных чипах, еще в Sun Microsystems, и продолжает использоваться сейчас:
Asynchronous & Synchronous Reset Design Techniques — Part Deux
Coding And Scripting Techniques For FSM Designs With Synthesis-Optimized, Glitch-Free Outputs
А вот любопытная статья, где вы увидите недодуманность верилога, которая осталась с 1980-х годов. Хотя сейчас, в эпоху static timing analysis, это не так актуально, но inertial и transport delays иногда упоминаются в литературе и коде, и стоит знать, как их моделировать:
Correct Methods For Adding Delays To Verilog Behavioral Models
Это я с Клиффом Каммингсом:
Автор: Юрий Панчул
