Проверка Netlist с использованием Yosys

Question

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

Теперь я хочу проверить правильность этого дизайна, вставив некоторые входы в список соединений и проверив вывод.

Например, я использовал контрольную метку s27 для своей модели, я хочу убедиться, что выход моей конструкции соответствует выходному знаку метки s27. Я прошел через руководство yosys, и я не мог понять, что это за команда. Кроме того, я использовал другие инструменты, такие как Veriwell. Но я действительно предпочитаю использовать yosys.

Answer 1

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

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

Следующий сценарий оболочки демонстрирует два различных элементарных методов формальной эквивалентности проверки после синтеза нетлисты с yosys:

# download fiedler-cooley.v 
if [ ! -f fiedler-cooley.v ]; then 
    wget https://raw.githubusercontent.com/cliffordwolf/yosys/master/tests/simple/fiedler-cooley.v 
fi 

# synthesis for ice40 
yosys -p 'synth_ice40 -top up3down5 -blif up3down5.blif' fiedler-cooley.v 

# formal verification with equiv_* 
yosys -l check1.log -p ' 
    # gold design 
    read_verilog fiedler-cooley.v 
    prep -top up3down5 
    splitnets -ports;; 
    design -stash gold 

    # gate design 
    read_blif up3down5.blif 
    techmap -autoproc -map +/ice40/cells_sim.v 
    prep -top up3down5 
    design -stash gate 

    # prove equivalence 
    design -copy-from gold -as gold up3down5 
    design -copy-from gate -as gate up3down5 
    equiv_make gold gate equiv 
    hierarchy -top equiv 
    equiv_simple 
    equiv_status -assert 
' 

# formal verification with BMC and temproral induction (yosys "sat" command") 
yosys -l check2.log -p ' 
    # gold design 
    read_verilog fiedler-cooley.v 
    prep -top up3down5 
    splitnets -ports;; 
    design -stash gold 

    # gate design 
    read_blif up3down5.blif 
    techmap -autoproc -map +/ice40/cells_sim.v 
    prep -top up3down5 
    design -stash gate 

    # prove equivalence 
    design -copy-from gold -as gold up3down5 
    design -copy-from gate -as gate up3down5 
    miter -equiv -flatten gold gate miter 
    hierarchy -top miter 
    sat -verify -tempinduct -prove trigger 0 -seq 1 -set-at 1 in_up,in_down 0 
' 

# formal verification with BMC+tempinduct using undef modeling 
yosys -l check3.log -p ' 
     # gold design 
     read_verilog fiedler-cooley.v 
     prep -top up3down5 
     splitnets -ports;; 
     design -stash gold 

     # gate design 
     read_blif up3down5.blif 
     techmap -autoproc -map +/ice40/cells_sim.v 
     prep -top up3down5 
     design -stash gate 

     # prove equivalence 
     design -copy-from gold -as gold up3down5 
     design -copy-from gate -as gate up3down5 
     miter -equiv -flatten -ignore_gold_x gold gate miter 
     hierarchy -top miter 
     sat -verify -tempinduct -prove trigger 0 -set-init-undef -set-def-inputs 
' 

Каждый метод формальной проверки эквивалентности имеет свои преимущества и недостатки.

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

Второй способ не должен соответствовать любым внутренним проводам по названию, но для этого требуется условие сброса для цепи (часть -seq 1 -set-at 1 in_up,in_down 0) и работает только с цепями, которые «просачивают» все внутреннее состояние на его выходы в пределах небольшого числа циклов независимо от последовательности входных сигналов.

Третий метод - это вариант второго метода, который использует моделирование состояний undef, чтобы избежать требования к условию сброса, но создает более сложную модель SAT и, следовательно, может быть менее эффективным вычислительно.

Чтобы все сказанное говорилось, вы никогда не должны полагаться на один инструмент, чтобы проверить, что сам результат произведен. Например. если в интерфейсе Yosys Verilog есть ошибка, то это также повлияет на синтез и проверку, и проблема никогда не будет обнаружена. Поэтому, если вы используете Yosys для проверки вывода Yosys, вы должны сделать это только в дополнение к схеме проверки, которая использует независимую базу кода. Например, Icarus Verilog или Verilator были бы двумя симуляторами, которые не разделяют никакого кода с Yosys (или друг другом afaict). Также: В общем, формальная проверка не заменяет симуляцию. (Специально не формальная проверка эквивалентности: откуда вы знаете, что модель, в которой вы проверяете эквивалентность, в первую очередь верна?)