Preview

Труды Института системного программирования РАН

Расширенный поиск

Поиск конфликтов доступа к данным в HDL-описаниях

https://doi.org/10.15514/ISPRAS-2019-31(3)-11

Аннотация

При проектировании модулей цифровой аппаратуры могут возникать конфликты доступа к данным. Одним из способов их выявления на ранних стадиях проектирования является статический анализ описаний цифровой аппаратуры (или HDL-описаний). В данной статье описывается метод поиска конфликтов доступа к данным в HDL-описаниях. Метод реализован в инструменте Retrascope и ориентирован на конфликты следующих типов: одновременные чтение и запись; одновременная запись; обращение к неинициализированным данным; отсутствие чтения между двумя актами записи. Конфликты задаются в виде условий (assertion) на внутренние переменные. Входное HDL-описание автоматически транслируется в формальную модель на языке, являющемся входным для инструмента проверки моделей nuXmv. Трансляция включает следующие этапы: 1) предварительная обработка; 2) построение графа потока управления; 3) трансформация графа потока управления в решающую диаграмму охраняемых действий (GADD-модель); 4) трансляция GADD-модели в формат инструмента nuXmv. Условия возникновения конфликтов строятся автоматически на основе статического анализа GADD-модели и передаются инструменту проверки моделей nuXmv. Найденные контрпримеры (последовательности значений входных сигналов, приводящие к достижению конфликта) автоматически транслируются инструментом Retrascope в тесты, которые могут быть исполнены на симуляторе. Предложенный метод поиска конфликтов был применен к ряду открытых тестовых наборов и модулей – Texas-97, Verilog2SMV, VCEGAR, mips16. Были выявлены потенциальные конфликты для всех указанных категорий. В качестве направлений дальнейших исследований рассматриваются вынос условий конфликтов на уровень входных сигналов (и получение, таким образом, сведений о протоколах взаимодействия между модулями), а также генерация встроенных проверок в коде HDL-описаний.

Об авторах

Александр Сергеевич Камкин
Институт системного программирования им. В.П. Иванникова РАН; Московский государственный университет им. М.В. Ломоносова; Московский физико-технический институт; Высшая школа экономики
Россия


Михаил Сергеевич Лебедев
Институт системного программирования им. В.П. Иванникова РАН
Россия


Сергей Александрович Смолов
Институт системного программирования им. В.П. Иванникова РАН
Россия


Список литературы

1. . S.Tahar, R. Kumar. Formal Verification of Pipeline Conflicts in RISC Processors. In Proc. of the European Design Automation Conference (EURO-DAC), 1994, pp. 285-289.

2. . M. Gordon,T. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993, 492 p.

3. . S. Hertz, D. Sheridan, S. Vasudevan. Mining Hardware Assertions with Guidance From Static Analysis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 32, No. 6, 2013, pp. 952-965.

4. . Cadence Incisive Formal Verifier. https://community.cadence.com//CSSharedFiles/forums/storage/22/10078/IncisiveFV_ds.pdf

5. . A.V. Aho, R. Sethi, J.D. Ullman. Compilers: principles, techniques, and tools. Addison-Wesley, 1986, 796 p.

6. . J. Brandt, M. Gemunde, K. Schneider, S. Shukla, J.-P. Talpin. Integrating system descriptions by clocked guarded actions. In Proc. of Forum on Specification and Design Languages (FDL), 2011, pp. 1-8.

7. . R. Cytron, J. Ferrante, B.K. Rosen, M.N. Wegman, F.K. Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, vol. 13, issue 4, 1991, pp. 451-490.

8. . A. Pnueli. The temporal logic of programs. In Proc. of the 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46-57.

9. . nuXmv model checker. https://nuxmv.fbk.eu

10. . Retrascope toolkit. https://forge.ispras.ru/projects/retrascope

11. . Texas-97 Verification Benchmarks. https://ptolemy.berkeley.edu/projects/embedded/research/vis/texas-97

12. . VCEGAR benchmark collection. https://www.cprover.org/hardware

13. . Verilog2SMV tool. https://es-static.fbk.eu/tools/verilog2smv

14. . Educational 16-bit MIPS Processor. https://opencores.org/projects/mips_16


Рецензия

Для цитирования:


Камкин А.С., Лебедев М.С., Смолов С.А. Поиск конфликтов доступа к данным в HDL-описаниях. Труды Института системного программирования РАН. 2019;31(3):135-144. https://doi.org/10.15514/ISPRAS-2019-31(3)-11

For citation:


Kamkin A.S., Lebedev M.S., Smolov S.A. Extracting Assertions for Conflicts in HDL Descriptions. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(3):135-144. https://doi.org/10.15514/ISPRAS-2019-31(3)-11



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)