~ cd 3.2. более сложные скрипты

3.2.1. Загрузка конструкции

read_verilog file1.v
read_verilog -I include_dir -D enable_foo -D WIDTH=12 file2.v
read_verilog -lib cell_library.v

verilog_defaults -add -I include_dir
read_verilog file3.v
read_verilog file4.v
verilog_defaults -clear

verilog_defaults -push
verilog_defaults -add -I include_dir
read_verilog file5.v
read_verilog file6.v
verilog_defaults -pop

Примечание: Фронтенд Verific для Yosys, который предоставляет команду verific, требует, чтобы Yosys был собран с Verific. Для полной функциональности требуются пользовательские модификации исходного кода Verific от YosysHQ, но ограниченная возможность использования может быть достигнута с некоторыми стоковыми сборками Verific. Подробнее о компиляции с помощью библиотеки Verific.

3.2.2. Selections

3.2.2.1. Framework selection

select foobar         # select the module foobar
delete                # delete selected objects

Обычно команда select перезаписывает предыдущее выделение. Команды select -add и select -del могут использоваться для добавления или удаления объектов из текущего выделения.

Команда select -clear может быть использована для сброса выбора к значению по умолчанию, которое представляет собой полный выбор всего в текущем модуле.

Этот фреймворк выбора также может быть использован непосредственно во многих других командах. Если в справке по использованию команды в качестве последнего аргумента указан [selection], это означает, что она будет использовать механизм, лежащий в основе select для оценки дополнительных аргументов и использования полученной выборки вместо выборки, созданной последней командой select.

Например, команда delete удалит все в текущем выделении, а delete foobar удалит только модуль foobar. Если команда select не была выполнена, то «текущим выбором» будет весь проект.

Примечание: Во многих примерах на этой странице используется команда show, чтобы наглядно продемонстрировать эффект от выбора.

3.2.2.2. Как сделать выбор

3.2.2.2.1. Выбор по имени объекта

select foobar         # select module foobar
select foo*           # select all modules whose names start with foo
select foo*/bar*      # select all objects matching bar* from modules matching foo*
select */clk          # select objects named clk from all modules

3.2.2.2.2. Модуль и конструкция в контексте

Команды могут выполняться в контексте module/ или design/. До сих пор все команды выполнялись в контексте конструкции. Для перехода в контекст модуля можно использовать команду cd.

cd foo                # switch to module foo
delete bar            # delete object foo/bar

cd mycpu              # switch to module mycpu
dump reg_*            # print details on all objects whose names start with reg_

cd ..                 # switch back to design

Примечание: Большинство сценариев синтеза никогда не переходят в контекст модуля. Но это очень мощный инструмент, который мы подробнее рассмотрим в интерактивное изучение конструкции.

3.2.2.2.3. Выбор по свойству или типу объекта

Для выбора по свойству или типу объекта можно использовать специальные шаблоны. Например:

• выберите все провода, чьи имена начинаются с reg_: select w:reg_*
• выберите все объекты с атрибутом foobar: select a:foobar
• выберите все объекты с атрибутом foobar, установленным на 42: select a:foobar=42
• выберите все модули с атрибутом blabla: select A:blabla
• выберите все ячейки $add из модуля foo: select foo/t:$add

Полный список выражений шаблона можно найти в ”разделе select — изменить и просмотреть список выбранных объектов”.

3.2.2.3. Операции по выделению

3.2.2.3.1. Комбинационное выделение

Команда select на самом деле гораздо мощнее, чем может показаться на первый взгляд. Когда она вызывается с несколькими аргументами, каждый аргумент оценивается и помещается в стек отдельно. После обработки всех аргументов он просто создает объединение всех элементов в стеке. Таким образом, select t:$add a:foo выберет все ячейки $add и все объекты с установленным атрибутом foo:

module foobaraddsub(a, b, c, d, fa, fs, ba, bs);
  input [7:0] a, b, c, d;
  output [7:0] fa, fs, ba, bs;
  assign fa = a + (* foo *) b;
  assign fs = a - (* foo *) b;
  assign ba = c + (* bar *) d;
  assign bs = c - (* bar *) d;
endmodule

yosys> select t:$add a:foo -list
foobaraddsub/$add$foobaraddsub.v:6$3
foobaraddsub/$sub$foobaraddsub.v:5$2
foobaraddsub/$add$foobaraddsub.v:4$1

Во многих случаях простое добавление все новых и новых элементов в выборку является неэффективным способом выделения интересной части конструкции. Для объединения элементов в стеке можно использовать специальные аргументы. Например, аргумент %i выхватывает из стека два последних элемента, пересекает их и помещает результат обратно в стек. Так, select t:$add a:foo %i выберет все ячейки $add, у которых установлен атрибут foo:

Листинг 3.40: Вывод для команды select t:$add a:foo %i -list в листинге 3.38

yosys> select t:$add a:foo %i -list
foobaraddsub/$add$foobaraddsub.v:4$1

• %u: объединение двух верхних элементов в стеке — pop 2, push 1
• %d: разность двух верхних элементов в стеке — pop 2, push 1
• %i: пересечение двух верхних элементов в стеке — pop 2, push 1
• %n: инверсия верхнего элемента в стеке — pop 1, push 1

Полный список см. в разделе «select — изменить и просмотреть список выбранных объектов«.

3.2.2.3.2. Расширение выбора

В листинге 3.41 используется нестандартный синтаксис Yosys {* … *} синтаксис для установки атрибута sumstuff на все ячейки, сгенерированные первым оператором assign. (Это работает с произвольными большими блоками кода Verilog и может быть использовано для пометки частей кода для анализа).

module sumprod(a, b, c, sum, prod);

  input [7:0] a, b, c;
  output [7:0] sum, prod;

  {* sumstuff *}
  assign sum = a + b + c;
  {* *}

  assign prod = a * b * c;

endmodule

Выбрав в этом модуле пункт a:sumstuff, вы получите следующую схему:

Поскольку выбраны только сами ячейки, но не временный провод $1_Y, два сумматора показаны как две разъединенные части. Это может быть очень полезно для глобальных сигналов, таких как тактовые сигналы и сигналы сброса: просто снимите их выделение с помощью такой команды, как select -del clk rst, и каждая ячейка, использующая их, получит свою собственную сетевую метку.

Однако в данном случае мы хотели бы видеть, что ячейки соединены правильно. Этого можно добиться с помощью параметра %x действие, которого расширяет выборку, то есть для каждого выбранного провода выбирает все ячейки, соединенные с проводом, и наоборот. Таким образом, show a:sumstuff %x дает диаграмму, показанную на рис. 3.12:

3.2.2.3.3. Выделение логических элементов

На рис. 3.12 показан так называемый входной конус суммы, т. е. все ячейки и сигналы, которые используются для генерации сигнала sum. Действие %ci может быть использовано для выбора входных конусов всех объектов в верхней выборке в стеке, поддерживаемом командой select.

Как и действие %x, эти команды расширяют выбор на один «шаг». Но на этот раз операция работает только против направления потока данных. То есть провода выбирают ячейки только через выходные порты, а ячейки выбирают провода только через входные порты.

Следующая последовательность диаграмм демонстрирует это пошаговое расширение:

Обратите внимание на тонкую разницу между show prod %ci и show prod %ci %ci. На обоих изображениях показана ячейка $mul, управляемая некоторыми входами $3_Y и c. Однако только на втором изображении, после второго вызова %ci, show может различить, что $3_Y — это провод, а c — вход. Мы можем увидеть это лучше с помощью команды dump:

  attribute \src "sumprod.v:4.21-4.25"
  wire width 8 output 5 \prod

  attribute \src "sumprod.v:10.17-10.26"
  cell $mul $mul$sumprod.v:10$4
    parameter \A_SIGNED 0
    parameter \A_WIDTH 8
    parameter \B_SIGNED 0
    parameter \B_WIDTH 8
    parameter \Y_WIDTH 8
    connect \A $mul$sumprod.v:10$3_Y
    connect \B \c
    connect \Y \prod
  end

  attribute \src "sumprod.v:10.17-10.22"
  wire width 8 $mul$sumprod.v:10$3_Y

  attribute \src "sumprod.v:3.21-3.22"
  wire width 8 input 3 \c

  attribute \src "sumprod.v:4.21-4.25"
  wire width 8 output 5 \prod

  attribute \src "sumprod.v:10.17-10.26"
  cell $mul $mul$sumprod.v:10$4
    parameter \A_SIGNED 0
    parameter \A_WIDTH 8
    parameter \B_SIGNED 0
    parameter \B_WIDTH 8
    parameter \Y_WIDTH 8
    connect \A $mul$sumprod.v:10$3_Y
    connect \B \c
    connect \Y \prod
  end

При выборе многих уровней логики повторять %ci снова и снова может быть скучновато. Для этого существует сокращение: к действию можно добавить количество итераций. Так, например, действие %ci3 идентично выполнению действия %ci три раза.

Действие %ci* выполняет действие %ci снова и снова, пока оно не перестанет действовать.

3.2.2.3.4. Усовершенствованная логика выделения конуса

В большинстве случаев существуют определенные типы ячеек и/или портов, которые не должны рассматриваться для действия %ci, или мы хотим отслеживать только определенные типы ячеек и/или портов. Этого можно добиться с помощью дополнительных шаблонов, которые могут быть добавлены к действию %ci.

Рассмотрим листинг 3.44. Он не служит никакой цели, кроме как быть нетривиальной схемой для демонстрации некоторых продвинутых возможностей Yosys.

module memdemo(clk, d, y);

input clk;
input [3:0] d;
output reg [3:0] y;

integer i;
reg [1:0] s1, s2;
reg [3:0] mem [0:3];

always @(posedge clk) begin
    for (i = 0; i < 4; i = i+1)
        mem[i] <= mem[(i+1) % 4] + mem[(i+2) % 4];
    { s2, s1 } = d ? { s1, s2 } ^ d : 4'b0;
    mem[s1] <= d;
    y <= mem[s2];
end

endmodule

Скрипт memdemo.ys используется для создания изображений, включенных в этот раздел. Давайте рассмотрим первую секцию:

Листинг 3.45: Синтез memdemo.v

read_verilog memdemo.v
prep -top memdemo; memory; opt

Там много чего происходит, но, возможно, нас интересует только дерево мультиплексоров, которые выбирают выходное значение. Для начала покажем только выходной сигнал y и его ближайших предшественников. Помня о выделении логических элементов, мы можем использовать show y %ci2:

Из этого мы узнаем, что y управляется ячейкой $dff, что y подключен к выходному порту Q, что сигнал clk поступает на входной порт CLK ячейки и что данные поступают из автоматически сгенерированного провода на вход D ячейки триггера (обозначается символом $ в начале имени). Теперь пойдем немного дальше и попробуем show y %ci5:

Это уже становится немного запутанным, поэтому, возможно, мы хотим игнорировать входы mux select. Чтобы добавить шаблон, мы добавляем двоеточие, за которым следует шаблон, к действию %ci. Сам шаблон начинается с символов — или +, указывающих на то, является ли он включающим или исключающим шаблоном, затем следует необязательный список типов ячеек, разделенных запятыми, за которым следует символ необязательный список имен портов в квадратных скобках, разделенных запятыми. В данном случае мы хотим исключить порт S типа ячейки $mux с помощью команды show y %ci5:-$mux[S]:

Мы могли бы использовать такую команду, как show y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff, в которой первый %ci перепрыгивает через начальный d-тип триггера, а второе действие выбирает весь входной конус, не переходя через входы выбора мультиплексора и ячейки триггера:

Или мы можем использовать show y %ci*:-[CLK,S]:+$dff:+$mux, следуя по входному конусу до конца, но только за ячейками $dff и $mux, и игнорируя любые порты с именами CLK или S:

Аналогично %ci существует действие %co для выбора выходных конусов, которое принимает тот же синтаксис для шаблона и повторения. Упомянутое ранее действие %x также принимает этот расширенный синтаксис.

Эти действия для обхода графа схемы в сочетании с действиями для булевых операций, таких как пересечение (%i) и разность (%d), которые являются мощными инструментами для выделения соответствующих частей исследуемой схемы.

3.2.2.3.5. Инкрементное выделение

select -none            # start with an empty selection
select -add reg_*       # select a bunch of objects
select -del reg_42      # but not this one
select -add state %ci   # and add more stuff

select t:$add t:$sub    # select all $add and $sub cells
select % %ci % %d       # select only the input wires to those cells

3.2.2.4. Сохранение и вызов выбранных элементов

Текущий выбор можно сохранить в памяти с помощью команды select -set <имя>. Позже его можно вызвать с помощью select @<имя>. Фактически, выражение @<имя> переносит сохраненный выбор в стек. Поддерживается командой select. Так, например, select @foo @bar %i выберет пересечение между хранящимися в памяти выборками foo и bar.

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

С помощью команды history можно получить список всех последних интерактивных команд. Эта возможность может быть полезна для создания сценария из команд, использованных в интерактивном сеансе.

Помните, что выражения select можно также использовать непосредственно в качестве аргументов большинства команд. Некоторые команды также принимают единственный аргумент select для некоторых параметров. В этих случаях для более сложного выбора необходимо использовать переменные select.

Пример кода из docs/source/code_examples/selections:

module test(clk, s, a, y);
    input clk, s;
    input [15:0] a;
    output [15:0] y;
    reg [15:0] b, c;

    always @(posedge clk) begin
        b <= a;
        c <= b;
    end

    wire [15:0] state_a = (a ^ b) + c;
    wire [15:0] state_b = (a ^ b) - c;
    assign y = !s ? state_a : state_b;
endmodule

Листинг 3.47: select.ys

...

Копировать

read_verilog select.v
prep -top test

cd test
select -set cone_a state_a %ci*:-$dff
select -set cone_b state_b %ci*:-$dff
select -set cone_ab @cone_a @cone_b %i
show -prefix select -format dot -notitle \
     -color red @cone_ab -color magenta @cone_a \
     -color blue @cone_b

3.2.3. Интерактивное изучение конструкции

3.2.3.1. Взгляд на команду show

В этом разделе рассматривается команда show и объясняются символы, используемые в генерируемых ею графических схемах. Используемый код включен в кодовую базу Yosys в разделе docs/source/code_examples/show.

3.2.3.1.1. Простая схема

В файле example.v приведен код Verilog для простой схемы, которую мы будем использовать для демонстрации применения show в простых условиях.

module example(input clk, a, b, c,
               output reg [1:0] y);
    always @(posedge clk)
        if (c)
            y <= c ? a + b : 2'd0;
endmodule

Сценарий синтеза Yosys, который мы будем запускать, приведен в листинге 3.49. Обратите внимание, что show вызывается с параметром -pause, которая останавливает выполнение сценария Yosys до тех пор, пока пользователь не нажмет клавишу Enter. Использование show

— pause также позволяет пользователю войти в интерактивную оболочку для дальнейшего изучения схемы перед продолжением синтеза.

Листинг 3.49: example_show.ys

read_verilog example.v
show -pause # first
proc
show -pause # second
opt
show -pause # third

Примечание: Изображения, используемые в этом документе, генерируются из файла example.ys, а не из файла example_show.ys. example.ys выводит схемы в виде файлов .dot, а не отображает их напрямую. Вы можете просмотреть эти изображения самостоятельно, запустив yosys example.ys, а затем xdot example_first.dot и т. д.

Первый вывод показывает проект непосредственно после его чтения внешним модулем Verilog. Входные и выходные порты отображаются в виде восьмиугольников. Ячейки отображаются в виде прямоугольников с входами слева и выходами справа. Метки ячеек состоят из двух строк: Первая строка содержит уникальный идентификатор ячейки, и вторая строка содержит тип ячейки. Внутренние типы клеток имеют префикс в виде знака доллара. Дополнительные сведения о внутренней библиотеке ячеек см. в разделе Внутренняя библиотека ячеек.

Константы отображаются в виде эллипсов, а значение константы — в виде метки. Используется синтаксис <bit_width>'<bits> для констант, ширина которых не 32 бита и/или которые содержат биты, не являющиеся 0 или 1 (например, x или z). Обычные 32-битные константы записываются с использованием десятичных чисел.

Однобитные сигналы показаны тонкими стрелками, направленными от источников к нагрузке. Сигналы шириной в несколько бит показаны в виде стрелок.

Наконец, процессы показаны в блоках с круглыми углами. Процессы — это внутреннее представление Yosys деревьев решений и событий синхронизации, смоделированных в блоке always Verilog. Метка гласит PROC, за которой в первой строке следует уникальный идентификатор, содержащий местоположение исходного кода оригинального блока always во второй строке. Обратите внимание, что мультиплексор из ?: — выражения представлен как ячейка $mux, но мультиплексор из if выражения все еще скрыт внутри процесса.

Команда proc преобразует процесс из первой диаграммы в мультиплексор и триггер d-типа, что приводит нас ко второй диаграмме:

Форма ромба справа — это висящий провод. (Проволочные узлы показаны только в том случае, если они висячие или имеют «известные» имена, например имена, назначенные из входных данных Verilog). Также обратите внимание, что в проекте теперь есть два экземпляра BUF-узла. Это объекты, оставленные командой proc. Это вполне обычное явление после вызова команд, выполняющих изменения в дизайне, поскольку большинство команд заботятся только о том, чтобы выполнить преобразование наименее сложным способом, а не об уборке после него. Следующий вызов clean (или opt , который включает clean в качестве одной из своих операций) очистит эти объекты. Эта операция настолько часто встречается в скриптах Yosys, что ее можно просто сократить с помощью лексемы ;;, которая служит разделителем команд. Если вы не хотите специально анализировать объекты, остающиеся после некоторых операций, рекомендуется всегда вызывать clean перед вызовом show .

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

Здесь мы видим, что команда opt не только удалила объекты, оставленные proc , но и правильно определила, что может удалить первую ячейку $mux без изменения поведения схемы.

3.2.3.1.2. Блоки выделения сигнальных векторов

В приведенном ниже листинге кода показана простая схема, в которой используется множество объединенных сигналов доступа.

module splice_demo(a, b, c, d, e, f, x, y);

input [1:0] a, b, c, d, e, f;
output [1:0] x;
assign x = {a[0], a[1]};

output [11:0] y;
assign {y[11:4], y[1:0], y[3:2]} =
                {a, b, -{c, d}, ~{e, f}};

endmodule

Обратите внимание, что вывод для этой схемы из команды show (рис. 3.27) выглядит довольно сложным. Это досадный побочный эффект того, что Yosys обрабатывает сигнальные векторы (они же многоразрядные провода или шины) как собственные объекты. Хотя это дает большие преимущества при анализе схем, оперирующих широкими целыми числами, это также вносит некоторую дополнительную сложность при обращении к отдельным битам сигнального вектора.

Ключевыми элементами для понимания этой схемы являются, конечно же, ячейки с круглыми углами и рядами, обозначенными <MSB_LEFT>:<LSB_LEFT> — <MSB_RIGHT>:<LSB_RIGHT>. Каждая из этих ячеек имеет один сигнал на ряд с одной стороны и общий сигнал для всех рядов с другой стороны. <MSB>:<LSB> указывают, какие биты сигналов разделяются и соединяются. Так, верхний ряд блока, соединяющего сигналы a и x, указывает, что бит 0 (т. е. диапазон 0:0) сигнала a соединен с битом 1 (т. е. диапазон 1:1) сигнала x.

Линии, соединяющие такие ячейки между собой, и линии, соединяющие такие ячейки с портами ячеек, имеют немного другой вид, чтобы подчеркнуть, что это не реальные сигнальные провода, а необходимость графического представления. Это различие кажется техническим, пока не возникает желание отладить проблему, связанную с тем, как Yosys внутренне представляет сигнальные векторы, например, при написании пользовательских команд Yosys.

3.2.3.1.3. Нетлисты уровня вентилей

На рис. 3.28 показаны две распространенные ошибки при работе с конструкциями, размещенные с библиотекой ячеек:

read_verilog cmos.v
prep -top cmos_demo
techmap
abc -liberty ../intro/mycells.lib;; 
show -format dot -prefix cmos_00

Во-первых, при создании этой диаграммы у Yosys не было доступа к библиотеке ячеек, в результате чего все порты ячеек по умолчанию оказались входами. Именно поэтому все порты нарисованы слева, а ячейки неудобно расположены в большом столбце. Во-вторых, двухбитный вектор y требует разбиения на ячейки для его отдельных битов, что приводит к излишней сложности диаграммы.

read_verilog cmos.v
prep -top cmos_demo
techmap
splitnets -ports
abc -liberty ../intro/mycells.lib;; 
show -lib ../intro/mycells.v -format dot -prefix cmos_01

Для рис. 3.29 в Yosys было передано описание библиотеки ячеек в виде файла Verilog, содержащего модули «черного ящика». Существует два способа загрузки описания ячеек в Yosys: Во-первых, Verilog-файл библиотеки ячеек может быть передан непосредственно команде show с помощью параметра -lib <filename>. Во-вторых, можно загрузить библиотеки ячеек в проект с помощью команды read_verilog -lib <filename>. Преимущество второго способа заключается в том, что библиотеку нужно загрузить только один раз и затем использовать ее во всех последующих вызовах команды show.

Кроме того, рис. 3.29 был сгенерирован после выполнения команды splitnet -ports. Эта команда разбивает все сигнальные векторы на отдельные сигнальные биты, что часто бывает необходимо при рассмотрении схем на уровне вентилей. Параметр -ports необходим, чтобы также разделить порты модулей. По умолчанию команда работает только с внутренними сигналами.

3.2.3.1.4. Прочие примечания

По умолчанию команда show выводит временный файл dot и запускает программу xdot для его отображения. Параметр -format, -viewer и -prefix могут быть использованы для изменения формата, средства просмотра и префикса имени файла. Обратите внимание, что форматы pdf и ps — единственные форматы, поддерживающие вывод нескольких модулей за один прогон. Формат dot можно использовать для вывода нескольких модулей, однако при попытке прочитать их xdot выдаст ошибку.

В плотно соединенных схемах иногда трудно уследить за отдельными сигнальными проводами. Для таких случаев полезно вызывать show с аргументом -colors <целое число>, который случайным образом назначает цвета для сети. Целое число (> 0) используется в качестве начального значения для случайного назначения цветов. Иногда необходимо перебрать несколько значений, чтобы найти подходящее назначение цветов.

Команда help show выводит полный список всех параметров, поддерживаемых командой show.

3.2.3.2. Навигация по конструкции

Построение принципиальных схем для целых модулей в проекте помогает только в простых случаях. Для сложных модулей сгенерированные принципиальные схемы получаются просто идиотски большими и не приносят никакой пользы. В таких случаях сначала нужно выделить соответствующие части схемы.

Помимо того, что отображать, необходимо также тщательно решить, когда это отображать, в отношении потока синтеза. Как правило, рекомендуется проводить диагностику схемы в самом раннем состоянии, в котором проблема может быть воспроизведена. Так, например, если внутреннее состояние перед вызовом команды techmap уже не удается проверить, лучше диагностировать corse-grain версию схемы до techmap, чем схему на уровне вентилей после techmap.

Примечание: Обычно рекомендуется проверять внутреннее состояние проекта, записывая его в Verilog-файл с помощью write_verilog -noexpr и используя имитационные модели из simlib.v и simcells.v из каталога данных Yosys (как выводится командой yosys-config —datdir).

3.2.3.2.1. Интерактивная навигация

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

В большинстве случаев оболочка запускается с выбором всего конструкции (т.е. когда сценарий синтеза еще не сузил выбор). Теперь можно использовать команду ls для создания списка всех модулей. Команду cd можно использовать для перехода к одному из модулей (для перехода обратно введите cd …). Теперь команда ls выводит список объектов в этом модуле. Это показано ниже на примере файла example.v из программы Простая схема.

yosys> ls

1 modules:
  example

yosys> cd example

yosys> ls

8 wires:
  $0\y[1:0]
  $add$example.v:5$2_Y
  $ternary$example.v:5$3_Y
  a
  b
  c
  clk
  y

2 cells:
  $add$example.v:5$2
  $ternary$example.v:5$3

1 processes:
  $proc$example.v:3$1

Когда модуль выбран с помощью команды cd, все команды (за некоторыми исключениями, такими как команды read_ и write_) работают только с выбранным модулем. Это также может быть полезно для скриптов синтеза, где различные стратегии синтеза должны применяться к разным модулям в конструкции.

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

Обычно вся интерактивная работа ведется с одним модулем, выбранным с помощью команды cd. Но можно работать и из дизайн-контекста (cd …). В этом случае все имена объектов должны иметь префикс <имя_модуля>/.

Например, a*/b* будет ссылаться на все объекты, чьи имена начинаются с b, из всех модулей, чьи имена начинаются с a.

Команда dump может быть использована для вывода всей информации об объекте. Например, вызов команды dump $2 после примера cd, приведенного выше:

attribute \src "example.v:5.22-5.27"
cell $add $add$example.v:5$2
  parameter \Y_WIDTH 2
  parameter \B_WIDTH 1
  parameter \A_WIDTH 1
  parameter \B_SIGNED 0
  parameter \A_SIGNED 0
  connect \Y $add$example.v:5$2_Y
  connect \B \b
  connect \A \a
end

Это может быть полезно, например, для определения имен сетей, подключенных к ячейкам, поскольку имена сетей обычно удаляются на схеме, если они генерируются автоматически. Обратите внимание, что вывод осуществляется в представлении RTLIL, описанном в RTLIL.

3.2.3.3. Интерактивное изучение конструкции

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

• Механизм выбора, особенно такие шаблоны, как %ci и %co, можно использовать для выяснения того, как связаны части конструкции.
• Такие команды, как submod, expose и splice, могут быть использованы для преобразования проекта в эквивалентный проект, который легче анализировать.
• Такие команды, как eval и sat, можно использовать для исследования поведения схемы.
• show — генерирование схем с помощью graphviz.
• dump — распечатать части конструкции в формате RTLIL.
• add — добавление объектов в конструкции и delete — удаление объектов в конструкции можно использовать для динамического изменения и реорганизации конструкции.

Используемый код включен в кодовую базу Yosys в разделе docs/source/code_examples/scrambler.

3.2.3.3.1. Изменение иерархии конструкции

Такие команды, как flatten и submod, могут использоваться для изменения иерархии проектирования, т. е. для уплощения иерархии или перемещения части модуля в подмодуль. Это находит применение в сценариях синтеза, а также при обратном проектировании и анализе. Ниже показан пример использования функции submod для реорганизации модуля в Yosys и проверки полученной схемы.

module scrambler(
        input clk, rst, in_bit,
        output reg out_bit
);
    reg [31:0] xs;
    always @(posedge clk) begin
        if (rst)
        xs = 1;
        xs = xs ^ (xs << 13);
        xs = xs ^ (xs >> 17);
        xs = xs ^ (xs << 5);
        out_bit <= in_bit ^ xs[0];
    end
endmodule

Листинг 3.56: scrambler.ys

...

Копировать

read_verilog scrambler.v

hierarchy; proc;;

cd scrambler
submod -name xorshift32 xs %c %ci %D %c %ci:+[D] %D %ci*:-$dff xs %co %ci %d

> cd xorshift32
> rename n2 in
> rename n1 out

> eval -set in 1 -show out
Eval result: \out = 270369.

> eval -set in 270369 -show out
Eval result: \out = 67634689.

> sat -set out 632435482
Signal Name                 Dec        Hex                                   Bin
-------------------- ---------- ---------- -------------------------------------
\in                   745495504   2c6f5bd0      00101100011011110101101111010000
\out                  632435482   25b2331a      00100101101100100011001100011010

3.2.3.3.2. Поведенческие изменения

Такие команды, как techmap, можно использовать для внесения изменений в поведение схемы, например, заменить асинхронный сброс на синхронный. Это находит применение в исследовании пространства проектирования (оценка различных архитектур для одной схемы).

(* techmap_celltype = "$adff" *)
module adff2dff (CLK, ARST, D, Q);

    parameter WIDTH = 1;
    parameter CLK_POLARITY = 1;
    parameter ARST_POLARITY = 1;
    parameter ARST_VALUE = 0;

    input CLK, ARST;
    input [WIDTH-1:0] D;
    output reg [WIDTH-1:0] Q;

    wire [1023:0] _TECHMAP_DO_ = "proc";

    wire _TECHMAP_FAIL_ = !CLK_POLARITY || !ARST_POLARITY;

    always @(posedge CLK)
        if (ARST)
            Q <= ARST_VALUE;
        else
            Q <= D;

endmodule

3.2.3.4. Усовершенствованные методы исследования

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

Вспомните конструкцию memdemo из раздела Усовершенствованная логика выделения элементов:

Поскольку в результате получается довольно большая схема, полезно разделить ее на более мелкие части для просмотра и работать с ним. В листинге 3.57 именно так и сделано: с помощью команды submod схема разбита на три секции: outstage, selstage и scramble.

select -set outstage y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff
select -set selstage y %ci2:+$dff[Q,D] %ci*:-$dff @outstage %d
select -set scramble mem* %ci2 %ci*:-$dff mem* %d @selstage %d
submod -name scramble @scramble
submod -name outstage @outstage
submod -name selstage @selstage

Параметр -name используется для указания имени нового модуля, а также имени новой ячейки в текущем модуле. Результирующие схемы показаны ниже.

3.2.3.4.1. Оценка комбинаторных схем

yosys [selstage]> eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1

1. Executing EVAL pass (evaluate the circuit given an input).
Full command line: eval -set s2,s1 4'b1001 -set d 4'hc -show n2 -show n1
Eval result: \n2 = 2'10.
Eval result: \n1 = 2'10.

Таким образом, параметр -set используется для установки входных значений, а параметра -show — для указания сетей для оценки.

Если параметр -show не указан, по умолчанию используются все выбранные порты вывода.

Если необходимое входное значение не задано, выдается ошибка. Вместо этого можно использовать параметр -set-undef, чтобы установить для всех неопределенных входных сетей значение undef (x).

yosys [selstage]> eval -set-undef -set d[3:1] 0 -table s1,d[0]

10. Executing EVAL pass (evaluate the circuit given an input).
Full command line: eval -set-undef -set d[3:1] 0 -table s1,d[0]

  \s1 \d [0] |  \n1  \n2
 ---- ------ | ---- ----
 2'00    1'0 | 2'00 2'00
 2'00    1'1 | 2'xx 2'00
 2'01    1'0 | 2'00 2'00
 2'01    1'1 | 2'xx 2'01
 2'10    1'0 | 2'00 2'00
 2'10    1'1 | 2'xx 2'10
 2'11    1'0 | 2'00 2'00
 2'11    1'1 | 2'xx 2'11

Assumed undef (x) value for the following signals: \s2

Предполагаемое значение undef (x) для следующих сигналов: \s2

Обратите внимание, что команда eval (как и команда sat, о которой пойдет речь в следующих разделах) выполняет только операцию на сглаженных модулях. Она не может анализировать сигналы, передаваемые через уровни иерархии проектирования. Поэтому команда flatten должна быть использована для модулей, содержащие экземпляры других модулей, прежде чем эти команды могут быть применены.

3.2.3.4.2. Решение комбинаторных задач SAT

Часто требуется противоположная команда eval, т.е. задан выход схемы, и мы хотим найти соответствующие входные сигналы. Для небольших схем с несколькими входными битами это можно сделать, перебирая все возможные комбинации входных сигналов, как это делает команда eval -table. Однако для больших схем Yosys предоставляет команду sat, которая использует SAT-решатель MiniSAT для решения такого рода задач.

Примечание: Хотя проверку модели можно выполнить непосредственно в Yosys, настоятельно рекомендуется использовать SBY или EQY для формальной верификации аппаратуры.

yosys [selstage]> sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001

11. Executing SAT pass (solving SAT problems in the circuit).
Full command line: sat -show s1,s2,d -set s1 s2 -set n2,n1 4'b1001

Setting up SAT problem:
Import set-constraint: \s1 = \s2
Import set-constraint: { \n2 \n1 } = 4'1001
Final constraint equation: { \n2 \n1 \s1 } = { 4'1001 \s2 }
Imported 3 cells to SAT database.
Import show expression: { \s1 \s2 \d }

Solving problem with 81 variables and 207 clauses..
SAT solving finished - model found:

  Signal Name                 Dec        Hex             Bin
  -------------------- ---------- ---------- ---------------
  \d                            9          9            1001
  \s1                           0          0              00
  \s2                           0          0              00

Обратите внимание, что команда sat поддерживает имена сигналов в обоих аргументах параметра -set. В примере выше мы использовали -set s1 s2, чтобы ограничить s1 и s2 равными. Когда требуются более сложные ограничения, необходимо построить схему-обертку, которая проверяет ограничения и сигнализирует о том, что ограничение выполнено, используя дополнительный выходной порт, который затем может быть принудительно приведен к значению с помощью опции -set. (Такая схема, содержащая тестируемую схему + дополнительные схемы проверки ограничений, называется miter-схемой).

module primetest(p, a, b, ok);
input [15:0] p, a, b;
output ok = p != a*b || a == 1 || b == 1;
endmodule

В листинге 3.58 показана схема, которую предполагается использовать в качестве теста на простое число. Если при заданном p для всех входных значений a и b значение ok равно 1, то p простое.

yosys [primetest]> sat -prove ok 1 -set p 31

1. Executing SAT pass (solving SAT problems in the circuit).
Full command line: sat -prove ok 1 -set p 31

Setting up SAT problem:
Import set-constraint: \p = 16'0000000000011111
Final constraint equation: \p = 16'0000000000011111
Imported 6 cells to SAT database.
Import proof-constraint: \ok = 1'1
Final proof equation: \ok = 1'1

Solving problem with 2790 variables and 8241 clauses..
SAT proof finished - model found: FAIL!

   ______                   ___       ___       _ _            _ _
  (_____ \                 / __)     / __)     (_) |          | | |
   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |
  |  ____/ ___) _ \ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|
  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_
  |_|   |_|   \___/ \___/ |_|       |_|  \_____|_|\_)_____)\____|_|


  Signal Name                 Dec        Hex                   Bin
  -------------------- ---------- ---------- ---------------------
  \a                        15029       3ab5      0011101010110101
  \b                         4099       1003      0001000000000011
  \ok                           0          0                     0
  \p                           31         1f      0000000000011111

Командной сессии интерпретатора Yosys, показанная в листинге 3.59, демонстрирует, что SAT-решатели могут находить даже неожиданные решения проблемы: используя целочисленное переполнение, на самом деле можно «факторизовать» 31. Разумеется, чистым решением было бы выполнить тест в 32 битах, например, заменив p != a*b в miter на p != {16’d0,a}b, или используя временную переменную для 32-битного произведения a*b. Но поскольку 31 хорошо укладывается в 8 бит, мы также можем просто заставить старшие 8 бит a и b обнулить для вызова sat, как это сделано ниже.

yosys [primetest]> sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0

1. Executing SAT pass (solving SAT problems in the circuit).
Full command line: sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0

Setting up SAT problem:
Import set-constraint: \p = 16'0000000000011111
Import set-constraint: { \a [15:8] \b [15:8] } = 16'0000000000000000
Final constraint equation: { \a [15:8] \b [15:8] \p } = { 16'0000000000000000 16'0000000000011111 }
Imported 6 cells to SAT database.
Import proof-constraint: \ok = 1'1
Final proof equation: \ok = 1'1

Solving problem with 2790 variables and 8257 clauses..
SAT proof finished - no model found: SUCCESS!

                  /$$$$$$      /$$$$$$$$     /$$$$$$$
                 /$$__  $$    | $$_____/    | $$__  $$
                | $$  \ $$    | $$          | $$  \ $$
                | $$  | $$    | $$$$$       | $$  | $$
                | $$  | $$    | $$__/       | $$  | $$
                | $$/$$ $$    | $$          | $$  | $$
                |  $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$
                 \____ $$$|__/|________/|__/|_______/|__/
                       \__/

Параметр -prove, используемый в листинге 3.60, работает аналогично -set, но пытается найти случай, когда два аргумента не равны. Если такой случай не найден, доказывается, что свойство выполняется для всех входов, удовлетворяющих остальным ограничениям.

Стоит отметить, что SAT-решатели не особенно эффективны при факторизации больших чисел. Но если небольшая проблема факторизации возникает как часть более крупной проблемы с цепями, SAT-решатель Yosys вполне способен ее решить.

3.2.3.4.3. Решение последовательных задач SAT

sat -seq 6 -show y -show d -set-init-undef \
  -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3

Параметр -seq 6 предписывает команде sat решить последовательную задачу за 6 временных шагов. (Эксперименты с меньшим числом шагов показали, что для приведения схемы в состояние, из которого может быть получена последовательность 1, 2, 3, требуется не менее 3 циклов).

Параметр -set-init-undef указывает команде sat инициализировать все регистры в состояние undef (x). То, как состояние x обрабатывается в Verilog, гарантирует, что решение будет работать при любом начальном состоянии.

Параметр -max_undef указывает команде sat найти решение с максимальным количеством undef.

Таким образом, мы можем четко видеть, какие биты входных данных имеют отношение к решению.

Наконец, третья опция -set-at добавляют ограничения для сигнала y на воспроизведение последовательности 1, 2, 3, начиная с временного шага 4.

Это дает следующий результат:

yosys [memdemo]> sat -seq 6 -show y -show d -set-init-undef \
    -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3

1. Executing SAT pass (solving SAT problems in the circuit).
Full command line: sat -seq 6 -show y -show d -set-init-undef
    -max_undef -set-at 4 y 1 -set-at 5 y 2 -set-at 6 y 3

Setting up time step 1:
Final constraint equation: { } = { }
Imported 29 cells to SAT database.

Setting up time step 2:
Final constraint equation: { } = { }
Imported 29 cells to SAT database.

Setting up time step 3:
Final constraint equation: { } = { }
Imported 29 cells to SAT database.

Setting up time step 4:
Import set-constraint for timestep: \y = 4'0001
Final constraint equation: \y = 4'0001
Imported 29 cells to SAT database.

Setting up time step 5:
Import set-constraint for timestep: \y = 4'0010
Final constraint equation: \y = 4'0010
Imported 29 cells to SAT database.

Setting up time step 6:
Import set-constraint for timestep: \y = 4'0011
Final constraint equation: \y = 4'0011
Imported 29 cells to SAT database.

Setting up initial state:
Final constraint equation: { \y \s2 \s1 \mem[3] \mem[2] \mem[1]
            \mem[0] } = 24'xxxxxxxxxxxxxxxxxxxxxxxx

Import show expression: \y
Import show expression: \d

Solving problem with 10322 variables and 27881 clauses..
SAT model found. maximizing number of undefs.
SAT solving finished - model found:

  Time Signal Name                 Dec        Hex             Bin
  ---- -------------------- ---------- ---------- ---------------
  init \mem[0]                      --         --            xxxx
  init \mem[1]                      --         --            xxxx
  init \mem[2]                      --         --            xxxx
  init \mem[3]                      --         --            xxxx
  init \s1                          --         --              xx
  init \s2                          --         --              xx
  init \y                           --         --            xxxx
  ---- -------------------- ---------- ---------- ---------------
     1 \d                            0          0            0000
     1 \y                           --         --            xxxx
  ---- -------------------- ---------- ---------- ---------------
     2 \d                            1          1            0001
     2 \y                           --         --            xxxx
  ---- -------------------- ---------- ---------- ---------------
     3 \d                            2          2            0010
     3 \y                            0          0            0000
  ---- -------------------- ---------- ---------- ---------------
     4 \d                            3          3            0011
     4 \y                            1          1            0001
  ---- -------------------- ---------- ---------- ---------------
     5 \d                           --         --            001x
     5 \y                            2          2            0010
  ---- -------------------- ---------- ---------- ---------------
     6 \d                           --         --            xxxx
     6 \y                            3          3            0011

Неудивительно, что на первом шаге решение устанавливает d = 0, поскольку это единственный способ установить регистры s1 и s2 в известное значение. Значения входных параметров для остальных шагов немного сложнее определить вручную, но SAT-решатель находит правильное решение мгновенно.

О команде sat можно написать еще много интересного. Например, есть набор параметров, которые можно использовать для выполнения последовательных доказательств с использованием темпоральной индукции. Команда help sat может быть использована для вывода списка всех параметров с кратким описанием их функций.

3.2.4. Проверка символьной модели

Примечание: Хотя проверку модели можно выполнить непосредственно в Yosys, настоятельно рекомендуется использовать SBY или EQY для формальной верификации аппаратуры.

Проверка символьной модели (SMC) используется для формального доказательства того, что схема обладает (или не обладает) заданным свойством.

Одно из применений — формальная проверка на эквивалентность: Доказательство того, что две схемы идентичны. Например, это очень полезная функция при отладке пользовательских команд в Yosys.

Среди других применений — проверка соответствия модуля стандартам интерфейса.

Команда sat в Yosys может использоваться для выполнения проверки символьной модели.

3.2.4.1. Проверка techmap

Давайте рассмотрим пример, включенный в кодовую базу Yosys в разделе docs/source/code_examples/ synth_flow:

module $add (A, B, Y);

parameter A_SIGNED = 0;
parameter B_SIGNED = 0;
parameter A_WIDTH = 1;
parameter B_WIDTH = 1;
parameter Y_WIDTH = 1;

input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
output [Y_WIDTH-1:0] Y;

generate
  if ((A_WIDTH == 32) && (B_WIDTH == 32))
    begin
      wire [16:0] S1 = A[15:0] + B[15:0];
      wire [15:0] S2 = A[31:16] + B[31:16] + S1[16];
      assign Y = {S2[15:0], S1[15:0]};
    end
  else
    wire _TECHMAP_FAIL_ = 1;
endgenerate

endmodule

module test(input [31:0]  a, b,
            output [31:0] y);
assign y = a + b;
endmodule

read_verilog techmap_01.v
hierarchy -check -top test
techmap -map techmap_01_map.v;;

# read test design
read_verilog techmap_01.v
hierarchy -top test

# create two version of the design: test_orig and test_mapped
copy test test_orig
rename test test_mapped

# apply the techmap only to test_mapped
techmap -map techmap_01_map.v test_mapped

# create a miter circuit to test equivalence
miter -equiv -make_assert -make_outputs test_orig test_mapped miter
flatten miter

# run equivalence check
sat -verify -prove-asserts -show-inputs -show-outputs miter

Solving problem with 945 variables and 2505 clauses..
SAT proof finished - no model found: SUCCESS!

3.2.4.2. Ведущий потока AXI4

Код, используемый в этом разделе, включен в кодовую базу Yosys в разделе docs/source/code_examples/axis.

Следующий ведущий потока AXI4 имеет ошибку. Но ошибка не проявляется, если ведомое устройство постоянно поддерживает tready. (То, что может сделать testbench).

Символическая проверка модели может быть использована для выявления ошибки и поиска последовательности значений для tready, которые приводят к неправильному поведению.

module axis_master(aclk, aresetn, tvalid, tready, tdata);
    input aclk, aresetn, tready;
    output reg tvalid;
    output reg [7:0] tdata;

    reg [31:0] state;
    always @(posedge aclk) begin
        if (!aresetn) begin
        state <= 314159265;
        tvalid <= 0;
        tdata <= 'bx;
    end else begin
        if (tvalid && tready)
            tvalid <= 0;
        if (!tvalid || !tready) begin
        //             ^- should not be inverted!
                state = state ^ state << 13;
                state = state ^ state >> 7;
                state = state ^ state << 17;
        if (state[9:8] == 0) begin
            tvalid <= 1;
            tdata <= state;
        end
        end
    end
    end
endmodule

module axis_test(aclk, tready);
    input aclk, tready;
    wire aresetn, tvalid;
    wire [7:0] tdata;

    integer counter = 0;
    reg aresetn = 0;

    axis_master uut (aclk, aresetn, tvalid, tready, tdata);

    always @(posedge aclk) begin
        if (aresetn && tready && tvalid) begin
        if (counter == 0) assert(tdata ==  19);
        if (counter == 1) assert(tdata ==  99);
        if (counter == 2) assert(tdata ==   1);
        if (counter == 3) assert(tdata == 244);
        if (counter == 4) assert(tdata == 133);
        if (counter == 5) assert(tdata == 209);
        if (counter == 6) assert(tdata == 241);
        if (counter == 7) assert(tdata == 137);
        if (counter == 8) assert(tdata == 176);
        if (counter == 9) assert(tdata ==   6);
        counter <= counter + 1;
    end
    aresetn <= 1;
    end
endmodule

read_verilog -sv axis_master.v axis_test.v
hierarchy -top axis_test

proc; flatten;;
sat -seq 50 -prove-assert

Solving problem with 159344 variables and 442126 clauses..
SAT proof finished - model found: FAIL!

Solving problem with 159144 variables and 441626 clauses..
SAT proof finished - no model found: SUCCESS!