| Verification of digital devices with concurrency behavior |
|
 |
|
|
| Authors |
| | Cheremisinov D.I. |
| | Cheremisinova L.D. |
| Date of publication |
| | 2020 |
| DOI |
| | 10.31114/2078-7707-2020-3-9-15 |
|
| Abstract |
| | The problem of verifying the functional correctness of implementations of reactive control systems with respect to their design specification is considered. When solving the problem of implementing control devices, one has to deal with the parallelism present in control objects. Such objects control goal is to ensure the coordinated operation of interacting components working asynchronously and in parallel. To describe the specification for such devices design it is proposed to use the PRALU language [6] of concurrent control algorithms, which allows temporal ordering of events that occur during operation of the control device.
The paper discusses the task of analyzing control device implementations for model input-output conformance [4, 5]. A methodology for constructing a test system for simulation based verification is proposed. Simulation of the control device for verification should be carried out in the area of its desired operation. Using the PRALU language to describe the control algorithm makes it possible to describe the behavior of the control system as a whole: not only the control algorithm, but also the behavior of the object controlled by the designed device. The control object is considered as part of the test environment. The implementation of the device under test is considered as a black box for which only inputs and outputs are available. Test sequences are generated dynamically - in the process of simulation of the control system.
Currently, there is software support for the automation of design and debugging of control systems, the design specification of which is in the PRALU language [21]. The software includes simulation tools and synthesizers of the PRALU language in the hardware models in the Verilog and C languages. |
| Keywords |
| | concurrent algorithm, hardware verification, simulation, PRALU language. |
| Library reference |
| | Cheremisinov D.I., Cheremisinova L.D. Verification of digital devices with concurrency behavior // Problems of Perspective Micro- and Nanoelectronic Systems Development - 2020. Issue 3. P. 9-15. doi:10.31114/2078-7707-2020-3-9-15 |
| URL of paper |
| | http://www.mes-conference.ru/data/year2020/pdf/D089.pdf |
