[VLSI CAD] kbdd - MiniSAT - Espresso - SIS?

Когда вы посещаете занятия по EDA или VLSI CAD, вам неожиданно представляют такие инструменты:

• kbdd
• MiniSAT
• Espresso
• SIS

Поначалу все они кажутся похожими: "Разве это не все о логических выражениях?"А разве мы когда-нибудь используем это на практике?"

В конечном счете, это инструменты из "мира чипов".

Эти базовые концепции используются во многих цифровых инструментах EDA, таких как логический синтез и DFT.

1. Общая картина: настоящая тема этого урока

Суть этого урока - как работать с булевыми функциями.

"Имеет ли эта логическая схема математический смысл?"

Для этого мы используем три различных подхода:

"Имеет ли эта логическая схема математический смысл?2. kbdd - "Та же логика, тот же график"Что делает kbdd

kbdd - это логический калькулятор, основанный на Двоичной диаграмме принятия решений (BDD).

Ключевым свойством BDD является следующее:Одна и та же булева функция всегда имеет одну и ту же структуру графа.

Иными словами:Не важно, насколько различны логические выраженияНе важно, насколько различна структура схемыЕсли функции одинаковы → BDD одинакова

Так что главное, что вы можете сделать с помощью kbdd, этоПроверка логической непротиворечивости (verify)Нахождение возможных комбинаций входных данных (satisfy)Удаление переменных (quantification)Автоматическое восстановление схем (logic repair)Когда используется kbddRTL vs Spec verificationGate-level logic debuggingFormal verification theory

👉 "Действительно ли эти две схемы - одно и то же?"
Это инструмент для ответа на этот вопрос математически.



Пример BDD показан ниже:

BDD - это дерево вопросов, представляющее "простое правило 0/1".

Для получения дополнительной информации см. документацию ниже:

https://www.sciencedirect.com/topics/computer-science/binary-decision-diagramПример: XOR f(x1,x2)=x1⊕x2Таблица истинности XOR:x1=0,x2=0→f=0x1=0,x2=1→f=1x1=1,x2=0→f=1x1=1,x2=1→f=0

Если мы превратим это в BDD, то для порядка переменных x1→x2:В корне (корневом узле) находится один узел x1.Из x1,если x1=0, мы спускаемся влево (0-край), иесли x1=1, мы спускаемся вправо (1-край).Ниже, у нас есть по одному из x2узлов.Из каждого узла x2 мы снова спускаемся внизслева, если x2=0, справа, если x2=1,и, наконец, приходим к Листу.

Мы можем нарисовать следующее.

Иными словами, это структура, которая "идет по ветвям 0/1 вдоль входного значения, а значение листа в конце - это значение булевой функции".Почему BDD хороша:Таблицы истинности имеют 2^n строк, поэтому они становятся сложными с ростом n.BDD уменьшает сложность Big(n), потому что может переиспользовать узлы, используя один и тот же шаблон.

Подведем итоги:BDD = "Для булевой функции направленный граф переменных → да/нет(0/1) ", поэтому вы можете ввести входные данные, пройтись по ветвям и автоматически прийти к результату.BDD - это структура, которая позволяет вам это сделать.