Extracting Assertions for Conflicts in HDL Descriptions

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

卷:31

Mikhail Sergeevitch Lebedev¹  Sergey Alexandrovitch Smolov²  Alexander Sergeevitch Kamkin³ 

[1] Московский государственный университет им. М.В. Ломоносова;

[2] Московский физико-технический институт;

[3] Институт системного программирования им. В.П. Иванникова РАН;

关键词: разработка аппаратуры;    язык описания аппаратуры;    функциональная верификация;    статический анализ;    генерация тестов;    конфликт доступа к данным;    граф потока управления;    охраняемое действие;    решающая диаграмма охраняемых действий;    проверка модели;   

DOI  :  10.15514/ISPRAS-2019-31(3)-11

来源: DOAJ

【 摘 要 】

Data access conflicts may arise in hardware designs. One of the ways of detecting such conflicts is static analysis of hardware descriptions in HDL. We propose a static analysis-based approach to data conflicts extraction from HDL descriptions. This approach has been implemented in the Retrascope tool. The following types of conflicts are considered: simultaneous reads and writes, simultaneous writes, reading of uninitialized data, no reads between two writes. Conflict assertions are formulated as conditions on variables. HDL descriptions are automatically translated into formal models suitable for the nuXmv model checker. The translation process consists of the following steps: 1) preliminary processing; 2) Control Flow Graph (CFG) building; 3) CFG transformation into a Guarded Actions Decision Diagram (GADD); 4) GADD translation into a nuXmv format. Conflict assertions are automatically built using static analysis of the GADD model and passed to the nuXmv model checker.  Bounded model checking is used to check whether these assertions are satisfiable. If true, counterexamples are generated and then translated to HDL testbenches by the Retrascope tool. The proposed approach was applied to several open source HDL benchmarks like Texas-97, Verilog2SMV, VCEGAR and mips16 modules. Potential conflicts have been detected for all of these benchmarks. Future work includes propagation of conflict assertions to the interface level (thus getting assertions on modules’ communication protocols) and generation of built-in HDL checkers.

【 授权许可】

Unknown