ABC: система для синтеза и формальной верификации последовательной логики

ABC постоянно меняется, но текущий снимок считается стабильным.

Компиляция:

Чтобы скомпилировать ABC как двоичный файл, загрузите и разархивируйте код, затем введите make. Чтобы скомпилировать ABC в виде статической библиотеки, введите make libabc.a.

При использовании ABC в качестве статической библиотеки предоставляются две дополнительные процедуры: Abc_Start() и Abc_Stop() для запуска и завершения работы фреймворка ABC в вызывающем приложении. Простая демонстрационная программа (файл src/demo.c) показывает, как создать автономную программу, выполняющую переписывание AIG с учётом DAG, путём вызова API ABC, скомпилированного в виде статической библиотеки.

Для создания демонстрационной программы:

• Скопируйте demo.c и libabc.a в рабочую директорию.
• Введите gcc -Wall -g -c demo.c -o demo.o.
• Введите g++ -g -o demo demo.o libabc.a -lm -ldl -lreadline -lpthread.

Чтобы запустить демонстрационную программу, предоставьте ей файл с логической сетью в формате AIGER или BLIF. Например:

[...] ~/abc> demo i10.aig
i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
Сети эквивалентны.
Чтение = 0,00 сек Переписывание = 0,18 сек Проверка = 0,41 сек

То же самое можно сделать, запустив двоичный файл в командном режиме:

[...] ~/abc> ./abc
UC Berkeley, ABC 1.01 (скомпилировано 6 октября 2012 г., 19:05:18)
abc 01> r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec
i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
Сети эквивалентны.

или в пакетном режиме:

[...] ~/abc> ./abc -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec"
Команда ABC: «r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec».
i10          : i/o =  257/  224  lat =    0  and =   2396  lev = 37
i10          : i/o =  257/  224  lat =    0  and =   1851  lev = 35
Сети эквивалентны.

Компиляция на C или C++

Текущую версию ABC можно скомпилировать с помощью компилятора C или компилятора C++.

• Чтобы скомпилировать как код C (по умолчанию): убедитесь, что CC=gcc и ABC_NAMESPACE не определены.
• Чтобы скомпилировать как код C++ без пространств имён: убедитесь, что CC=g++ и ABC_NAMESPACE не определено.
• Чтобы скомпилировать как код C++ с пространствами имён: убедитесь, что CC=g++ и ABC_NAMESPACE установлены на имя запрошенного пространства имён. Например, добавьте -DABC_NAMESPACE=xxx к OPTFLAGS.

Создание общей библиотеки

• Скомпилируйте код как независимый от позиции, добавив ABC_USE_PIC=1.

• Создайте цель libabc.so:

  make ABC_USE_PIC=1 libabc.so

Отчёт об ошибках:

Пожалуйста, попробуйте воспроизвести все обнаруженные ошибки и неожиданные функции, используя последнюю доступную версию ABC по адресу https://github.com/berkeley-abc/abc. Если ошибка всё ещё сохраняется, пожалуйста, предоставьте следующую информацию:

1. Версия ABC (когда она была загружена с GitHub).
2. Дистрибутив Linux и версия (32-разрядная или 64-разрядная).
3. Точная команда и сообщение об ошибке при попытке запустить инструмент.
4. Вывод команды ldd, запущенной на исполняемом файле (например, ldd abc).
5. Версии соответствующих инструментов или пакетов, которые использовались.

Устранение неполадок:

1. Если компиляция не начинается из-за проверки циклической зависимости, попробуйте коснуться всех файлов следующим образом: find ./ -type f -exec touch "{}" \;
2. Если компиляция завершается неудачно из-за отсутствия readline, установите библиотеку readline или скомпилируйте с make ABC_USE_NO_READLINE=1
3. Если компиляция завершается неудачно из-за отсутствия pthreads, установите библиотеку pthreads или скомпилируйте с make ABC_USE_NO_PTHREADS=1
   • См. http://sourceware.org/pthreads-win32/ для pthreads в Windows.
   • Доступны предварительно скомпилированные DLL-файлы с ftp://sourceware.org/pub/pthreads-win32/dll-latest.
4. Если компиляция завершается неудачей в файле... «src/base/main/libSupport.c», попробуйте следующее:

• Удалите «src/base/main/libSupport.c» из «src/base/main/module.make».
• Закомментируйте вызовы Libs_Init() и Libs_End() в «src/base/main/mainInit.c».

1. В некоторых системах для работы readline требуется добавить '-lcurses' в Makefile.

Комментарий от Криша Сундаресана:

«Я обнаружил, что код корректно компилируется на Solaris, если использовать gcc (вместо g++, который я по какой-то причине использовал). Также readline, который по умолчанию недоступен в большинстве систем Sol10, необходимо установить. Я скачал пакет readline-5.2 с сайта sunfreeware.com и установил его локально. Также изменил CFLAGS, чтобы добавить локальные файлы include для readline, и LIBS, чтобы добавить локальный libreadline.a. Возможно, вы можете добавить эти шаги в файл readme, чтобы помочь людям, которые компилируют это на Solaris».

Учебник любезно предоставлен Аной Петковской из EPFL: https://www.dropbox.com/s/qrl9svlf0ylxy8p/ABC_GettingStarted.pdf

Заключительные замечания:

К сожалению, нет комплексного регрессионного теста. Удачи!

Эту систему поддерживает Алан Мищенко alanmi@berkeley.edu. Рассмотрите также использование фреймворка ZZ, разработанного Никласом Ином: https://bitbucket.org/niklaseen/abc-zz (или https://github.com/berkeley-abc/abc-zz).