Simulation and analysis of digital sytems

Dipartimento di Ingegneria dell'informazione, Università di Pisa


This page is a summary of the research activities on simulation and analysis of digital sytems, based on formal methods, carried out at the Department of Information Engineering at the University of Pisa.

Co-simulation and formal integrated development environments


[SEFM 2017]
Andrea Domenici, Adriano Fagiolini, Maurizio Palmieri. Integrated simulation and formal verification of a simple autonomous vehicle , In 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems, Trento, Italy, September 5, 2017 (in press).

abstract  This paper presents a proof-of-concept application of an approach to system development based on the integration of formal verification and co-simulation. A simple autonomous vehicle has the task of reaching an assigned straight path and then follow it, and it can be controlled by varying its turning speed. The correctness of the proposed control law has been formalized and verified by interactive theorem proving with the Prototype Verification System. Concurrently, the system has been co-simulated using the Prototype Verification System and the MathWorks Simulink tool: The vehicle kinematics have been simulated in Simulink, whereas the controller has been modeled in the logic language of the Prototype Verification System and simulated with the interpreter for the same language available in the theorem proving environment. With this approach, co-simulation and formal verification corroborate each other, thus strengthening developers' confidence in their analysis.

[IE3TSE 2017]
Cinzia Bernardeschi, Andrea Domenici, Paolo Masci A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems , IEEE Transactions on Software Engineering, vol. PP, 2017. [ bib |  DOI |  draft ]

abstract  This paper presents a methodology, with supporting tool, for formal modeling and analysis of software components in cyber-physical systems. Using our approach, developers can integrate a simulation of logic-based specifications of software components and Simulink models of continuous processes. The integrated simulation is useful to validate the characteristics of discrete system components early in the development process. The same logic-based specifications can also be formally verified using the Prototype Verification System (PVS), to gain additional confidence that the software design complies with specific safety requirements. Modeling patterns are defined for generating the logic-based specifications from the more familiar automata-based formalism. The ultimate aim of this work is to facilitate the introduction of formal verification technologies in the software development process of cyber-physical systems, which typically requires the integrated use of different formalisms and tools. A case study from the medical domain is used to illustrate the approach. A PVS model of a pacemaker is interfaced with a Simulink model of the human heart. The overall cyber-physical system is co-simulated to validate design requirements through exploration of relevant test scenarios. Formal verification with the PVS theorem prover is demonstrated for the pacemaker model for specific safety aspects of the pacemaker design.

[F-IDE 2016]
Gioacchino Mauro, Harold Thimbleby, Andrea Domenici, Cinzia Bernardeschi. Extending a user interface prototyping tool with automatic MISRA C code generation , In 3rd Workshop on Formal Integrated Development Environment (F-IDE 2016), Limassol, Cyprus, November 8, 2016. [ bib |  DOI |  http  |   slides ]

abstract  We are concerned with systems, particularly safety-critical systems, that involve interaction between users and devices, such as the user interface of medical devices. We therefore developed a MISRA C code generator for formal models expressed in the PVSio-web prototyping toolkit. PVSio-web allows developers to rapidly generate realistic interactive prototypes for verifying usability and safety requirements in human-machine interfaces. The visual appearance of the prototypes is based on a picture of a physical device, and the behaviour of the prototype is defined by an executable formal model. Our approach transforms the PVSio-web prototyping tool into a model-based engineering toolkit that, starting from a formally verified user interface design model, will produce MISRA C code that can be compiled and linked into a final product. An initial validation of our tool is presented for the data entry system of an actual medical device.
[CARDIOTECHNIX 2014]
Cinzia Bernardeschi, Andrea Domenici, and Paolo Masci. Integrated Simulation of Implantable Cardiac Pacemaker Software and Heart Models. 2d International Congress on Cardiovascular Technology (CARDIOTECHNIX 2014), Rome, Italy, 2014. [ bib | slides | http | CARDIOTECHNIX 2014 web site ]

abstract  This paper presents an approach for integrated simulation of pacemaker models and heart models, each developed with the appropriate formalism. Heart models are developed in MathWorks, a powerful tool for the simulation of complex systems, whereas pacemakers are developed in PVS, a theorem-proving environment enabling both simulation and formal verification of safety requirements. The two tools communicate over a Web-based interface, which makes it possible to integrate the simulation of the MathWorks model of the heart and the PVS model of the pacemaker. In this paper, we illustrate the architecture developed for integrated simulation of the pacemaker-heart system and present an example application for realistic models.

Higher-order logic

The higher-order logic language of the Prototype Verification System has been used to formalize, verify, and simulate systems with dependability constraints.
[ICT4eHEALTH 2016]
Cinzia Bernardeschi, Andrea Domenici, Paolo Masci. Modeling Communication Network Requirements for an Integrated Clinical Environment in the Prototype Verification System , In 4th ICTS4eHealth Workshop, 2016 IEEE Symposium on Computers and Communication (ISCC), Messina, Italy, June 27 - 30, 2016. [ bib |  DOI |  http ]

abstract  Health care practices increasingly rely on complex technological infrastructure, and new approaches to the integration of information and communication technology in those practices lead to the development of such concepts as integrated clinical environments and smart intensive care units. These concepts refer to hospital settings where therapy relies heavily on inter-operating medical devices, supervised by clinicians assisted by advanced monitoring and co-ordinating software. In order to ensure safety and effectiveness of patient care, it is necessary to specify the requirements of such socio-technical systems in the most rigorous and precise way. This paper presents an approach to the formalization of system requirements for communication networks deployed in integrated clinical environment, based on the higher-order logic language of a theorem-proving environment, the Prototype Verification System.
[IPL 2016]
Cinzia Bernardeschi, Andrea Domenici. Verifying safety properties of a nonlinear control by interactive theorem proving with the Prototype Verification System , Information Processing Letters vol. 116, no. 6, pp. 409--415, 2015. [ bib |  DOI |  http |  preprint ]

abstract  Interactive, or computer-assisted, theorem proving is the verification of statements in a formal system, where the proof is developed by a logician who chooses the appropriate inference steps, in turn executed by an automatic theorem prover. In this paper, interactive theorem proving is used to verify safety properties of a nonlinear (hybrid) control system.
[MOBIHEALTH 2015]
Cinzia Bernardeschi, Andrea Domenici, Paolo Masci. Towards a Formalization of System Requirements for an Integrated Clinical Environment In 5th EAI International Conference on Wireless Mobile Communication and Healthcare (MOBIHEALTH 2015) London, October 14-16, 2015. [ bib |  DOI |   http ]

abstract  Interoperability of medical devices, and their interface to clinicians and patients, are critical issues for the safety and effectiveness of patient care. Ongoing efforts strive at establishing standards for integrated clinical environments, which may connect and co-ordinate several medical devices and interface them to patients, clinicians, and hospital information systems. In this paper, an approach to the formalization of system requirements for an integrated clinical environment is presented. The formalization relies on the higher-order logic language of the Prototype Verification System.
[IJAS 2011]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, and Paolo Masci. Simulation and Test-Case Generation for PVS Specifications of Control Logics. International Journal on Advances in Software, 4(3 & 4):327-341, 2011. [ bib | http]

abstract  We describe a framework for the simulation of control logics specified in the higher-order logic of the Prototype Verification System. The framework offers a library of predefined modules, a method for the composition of more complex modules, and an event-driven simulation engine. A developer defines a system architecture by composing its model out of library modules, possibly introducing new module definitions, and simulates the behaviour of the system model by providing its input waveforms, which are given as functions from time to logic levels. The generation of simulation scenarios (test cases) can be automated by using parametric waveforms that can be instantiated through universal and existential quantifiers. We demonstrate the simulation capabilities of our framework on two simple case studies from a nuclear power plant application. The main feature of this approach is that our formal specifications are executable. Moreover, once the simulation experiments give developers sufficient confidence in the correctness of the specification, the logic models can serve as the basis for its formal verification.

[COMPUTATION TOOLS 2010]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, and Paolo Masci. Debugging PVS specifications of control logics via event-driven simulation. In Computation Tools 2010, Lisbon, Portugal, November 21-26 2010. IARIA. [ bib ]

abstract  In this paper we present a framework aimed at simulating control logics specified in the higher-order logic of the Prototype Verification System (PVS). The framework offers a library of predefined modules, a method for the composition of more complex modules, and an event-driven simulation engine. A developer simulates the specified system by providing its input waveforms as functions from time to logic levels. Once the simulation experiments give sufficient confidence in the correctness of the specification, the model can serve as a basis for the formal verification of desired properties of interest. A simple case study from a nuclear power plant application is shown.

Stochastic Activity Networks

The ASSESS tool is a simulator based on a Stochastic Activity Networks model of digital circuits, which has been used for the simulation and analysis of the effects of Single Event Upsets in SRAM-based FPGAs. The simulator is built upon the Möbius tool and works in conjunction with an EDIF parser and external tools, such as E2STAR and GABES.

[PhD THESIS]
Luca Cassano. Analysis and Test of the Effects of Single Event Upsets Affecting the Configuration Memory of SRAM-based FPGAs. Ph.D. thesis, Dottorato di Ricerca in Ingegneria dell'informazione, Scuola di Dottorato in Ingegneria "Leonardo da Vinci", Università di Pisa. 2013. (Winner of the European semi-finals of the TTTC's E. J. McCluskey Doctoral Thesis Award, 2014). [ http |

[IE3TCAD 2014]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Luca Sterpone. ASSESS: A Simulator of Soft Errors in the Configuration Memory of SRAM-Based FPGAs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 33, no. 9, pp. 1342-1355, Sept. 2014. [ bib |  DOI |  draft ]

abstract  In this paper a simulator of soft errors (SEUs) in the configuration memory of SRAM-based FPGAs is presented. The simulator, named ASSESS, adopts fault models for SEUs affecting the configuration bits controlling both logic and routing resources that have been demonstrated to be much more accurate than classical fault models adopted by academic and industrial fault simulators currently available. The simulator permits the propagation of faulty values to be traced in the circuit, thus allowing the analysis of the faulty circuit not only by observing its output, but also by studying fault activation and error propagation. ASSESS has been applied to several designs, including the miniMIPS microprocessor, chosen as a realistic test case to evaluate the capabilities of the simulator. The ASSESS simulations have been validated comparing their results with a fault injection campaign on circuits from the ITC'99 benchmark, resulting in an average error of only 0.1%.

[IECON 2013]
Federico Baronti, Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Roberto Roncella, and Roberto Saletti. Mitigation of Single Event Upsets in the Control Logic of a Charge Equalizer for Li-ion Batteries. In 39th Annual Conference of the IEEE Industrial Electronics Society (IECON 2013), Vienna, Austria, 2013. [ bib |  DOI |  slides ]

abstract  Lithium-ion batteries are increasingly being used in safety-critical applications, such as automotive, avionics and aerospace systems. They require the adoption of an electronic control system, called Battery Management System (BMS), to guarantee their safe and effective operation. Therefore, the reliability of the BMS is of paramount importance. In this paper, we analyze the effects of Single Event Upsets (SEUs) occurring in the control logic of an important BMS subsystem, i.e., the charge equalizer. Moreover, some SEU mitigation techniques based on logic redundancy are presented and their effectiveness is compared through fault simulation.

[JSA 2013]
Cinzia Bernardeschi, Luca Cassano, Mario G. C. A. Cimino, and Andrea Domenici. GABES: a Genetic Algorithm Based Environment for SEU Testing in SRAM-FPGAs, Journal of Systems Architecture, vol. 59, pages 1383-1254, 2013. [ bib |  DOI |  draft ]

abstract  Testing of FPGAs is gaining more and more interest because of the application of FPGA devices in many safety-critical systems. We propose GABES, a tool for the generation of test patterns for application-dependent testing of SEUs in SRAM-FPGAs, based on a genetic algorithm. Test patterns are generated and selected by the algorithm according to their fault coverage: Faults are injected in a simulated model of the circuit, the model is executed for each test pattern and the respective fault coverage is computed. We focus on SEUs in configuration bits affecting logic resources of the FPGA. This makes our fault model much more accurate than the classical stuck-at model. Results from the application of the tool to some circuits from the ITC'99 benchmarks are reported. These results suggest that this approach may be effective in the inspection of safety-critical components of control systems implemented on FPGAs.

[DFT 2012]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, and Luca Sterpone. Accurate Simulation of SEUs in the Configuration Memory of SRAM-based FPGAs. In Proceedings of the 25th IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems (DFT2012), pages 115-120, IEEE, 2014. [ bib | DOI ]

abstract  SRAM-based FPGAs are more and more relevant in a growing number of applications, ranging from the automotive to the aerospace ones. Designers of safety-critical applications demand accurate methodologies to evaluate the Single Event Upsets (SEUs) sensitivity of their designs. In this paper, we present an accurate simulation method for the evaluation of the effects of SEUs in the configuration memory of SRAM-based FPGAs. The approach is able to simulate SEUs affecting the configuration memory of both logic and routing resources since it is able to accurately model the electrical behavior of SEUs in the configuration memory. Detailed experimental results on a large set of benchmark circuits are provided and the comparison with fault injection experiments is shown in order to validate the accuracy of the proposed method. The results clearly demonstrate the benefits of our approach since simulation results predict almost completely the results obtained through fault injection.

[WRC 2012]
Cinzia Bernardeschi, Luca Cassano, Mario Giovanni Cosimo Antonio Cimino, and Andrea Domenici. Application of a Genetic Algorithm for Testing SEUs in SRAM-FPGA Systems. In 6th HiPEAC Workshop on Reconfigurable Computing (WRC 2012), 2012. [ bib| http  ]

abstract  Testing of FPGAs is gaining more and more interest because of the employment of FPGA devices in many safety-critical application fields. We propose a prototype of a tool for the generation of test patterns for application-dependent testing of SEUs in SRAM-FPGAs based on a genetic algorithm. We focus on SEUs affecting logic resources of the FPGA. SEUs in any configuration bit are addressed, making our fault model much more accurate than the classical stuck-at fault model. Results from the application of the tool to some circuits from the ISCAS and ITC benchmarks are reported.

[COMPUTATION TOOLS 2011]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, and Paolo Masci. A Tool for Signal Probability Analysis of FPGA-Based Systems. In Proceedings of the 2nd International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking (COMPUTATION TOOLS 2011), pages 13-18, 2011. [ bib ]

abstract  We describe a model of Field Programmable Gate Array based systems realised with the Stochastic Activity Networks formalism. The model can be used (i) to debug the circuit design synthesised from the high level description of the system, and (ii) to calculate the signal probabilities and transition densities of the circuit design, which are parameters that can be used for reliability analysis, power consumption estimation and pseudo random testing. We validate the developed model by reproducing the results presented in other studies for some representative combinatorial circuits, and we explore the applicability of the proposed model in the analysis of real-world devices by analysing the actual implementation of a circuit for the generation of Cyclic Redundancy Check codes.

[FPL 2011]
Cinzia Bernardeschi, Luca Cassano, and Andrea Domenici. Failure Probability and Fault Observability of SRAM-FPGA Systems. In International Conference on Field Programmable Logic and Applications (FPL2011), pages 385-388. IEEE, sep 2011. [ bib | DOI ]

abstract  We describe a simulation-based fault injection technique for failure probability and fault observability assessment of SRAM-FPGA systems. Our approach relies on a model of FPGA netlists realised with the Stochastic Activity Networks formalism. Faults can be injected into the model either stochastically or exhaustively one at a time. Fault propagation is traced to the output pins, using a four-valued logic that enables faulty signals to be tagged and recognized. We considered some of the ITC'99 benchmarks as examples.

[DDECS 2011]
Cinzia Bernardeschi, Luca Cassano, and Andrea Domenici. Failure probability of SRAM-FPGA systems with Stochastic Activity Networks. In IEEE 14th International Symposium on Design and Diagnostics of Electronic Circuits Systems (DDECS 2011), pages 293-296. IEEE, apr 2011. [ bib | DOI ]

abstract  We describe a simulation-based fault injection technique for calculating the probability of failures caused by SEUs in the configuration memory of SRAM-FPGA systems. Our approach relies on a model of FPGA netlists realised with the Stochastic Activity Networks (SAN) formalism. We validate our method by reproducing the results presented in other studies for some representative combinatorial circuits, and we explore the applicability of the proposed technique by analysing the actual implementation of a circuit for the generation of Cyclic Redundancy Check codes.

[VALID 2011]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Giancarlo Gennaro, and Mario Pasquariello. Simulated Injection of Radiation-Induced Logic Faults in FPGAs. In Proceedings of the 3rd International Conference on Advances in System Testing and Validation Lifecycle (VALID 2011), pages 84-89. IARIA, 2011. [ bib | http]

abstract  SRAM-FPGA systems are simulated with a model based on the Stochastic Activity Networks (SAN) formalism. Faults are injected into the model and their propagation is traced to the output pins using a four-valued logic that enables faulty logical signals to be tagged and recognized without recurring to a comparison with the expected output values. Input vectors are generated probabilistically based on assumed signal probabilities. By this procedure it is possible to obtain a statistical assessment of the observability of different faults for the generated inputs. The analysis of a 2-out-of-2 voter is shown as a case study.

Model checking

Model checking techniques have been used, with the SAL framework, to prove the unexcitability or untestability of faults induced by SEU in SRAM-based FPGAs.

[IVLSIJ 2016]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Luca Sterpone. UA2TPG: An Untestability Analyzer and Test Pattern Generator for SEUs in the Configuration Memory of SRAM-based FPGAs , Integration, the VLSI Journal, vol. 55, pp. 85--97, 2016. [ bib |  DOI |   http ]

abstract  This paper presents UA2TPG, a static analysis tool for the untestability proof and automatic test pattern generation for SEUs in the configuration memory of SRAM-based FPGA systems. The tool is based on the model-checking verification technique. An accurate fault model for both logic components and routing structures is adopted. Experimental results show that many circuits have a significant number of untestable faults, and their detection enables more efficient test pattern generation and on-line testing. The tool is mainly intended to support on-line testing of critical components in FPGA fault-tolerant systems.

[IE3TII 2014]
Federico Baronti, Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Roberto Roncella, and Roberto Saletti. Design and Safety Verification of a Distributed Charge Equalizer for Modular Li-ion Batteries. IEEE Transactions on Industrial Informatics, vol. 10, no. 2, pp. 1003-1011, May 2014. [ bib |  DOI ]

abstract  This paper presents a novel charge equalization technique seamlessly integrated into a modular Battery Man- agement System (BMS) for lithium-ion (Li-ion) batteries. The charge equalizer is a crucial element for an effective use of a Li- ion battery consisting of many series-connected cells. We describe a fully distributed charge equalizer, based on a circular balancing bus, which outperforms other recently published approaches. Its safety requirements have formally been verified using a model checker, showing that formal methods, and in particular the Symbolic Analysis Laboratory environment, can be effective to verify the safety requirements of a BMS.

[GLSVLSI 2013]
Cinzia Bernardeschi, Luca Cassano, and Andrea Domenici. Unexcitability Analysis of SEUs Affecting the Routing Structure of SRAM-based FPGAs. In Proceedings of the 23rd ACM International Conference on Great Lakes Symposium on VLSI (GLSVLSI'13), pages 7-12, ACM, 2013. [ bib | DOI |  preprint ]

abstract  Testing SEUs in the configuration memory of SRAM-based FPGAs is very costly due to their large configuration memory, therefore it is necessary to optimize the generation of test patterns. In particular, in order to reduce the effort required of automatic test pattern generators, it is useful to identify early the unexcitable faults, i.e., those faults that cannot be excited by any combination of input signals. In this paper, the unexcitability of SEUs affecting the configuration bits controlling the routing resources of SRAM-based FPGAs is considered. Since this part of the configuration memory contains the largest number of configuration bits, its testing is particularly onerous. Faults in the routing resources are modeled considering the actual electrical behavior of the affected interconnections, thus the resulting fault model is more accurate than the classical open/short model usually considered. This paper introduces a methodology to prove the unexcitability of these faults. The methodology has been implemented in a tool based on a formal specification language (SAL) and a model checker (SAL-SMC). Results from the application of the tool to some circuits from the ITC'99 benchmark are reported.

[IOLTS 2012]
Cinzia Bernardeschi, Luca Cassano, and Andrea Domenici. SEU-X: A SEu un-eXcitability prover for SRAM-FPGAs. In 2012 IEEE 18th International On-Line Testing Symposium (IOLTS), pages 25-30, jun 2012. [ bib | DOI ]

abstract  We propose an untestability prover for Single Event Upset (SEU) faults affecting the configuration memory of logic resources of SRAM-FPGA systems. In particular we focus on the subset of untestable faults that can not even be excited, with the aim of optimizing the generation of test patterns, in particular for in-service testing. SEUs in configuration bits of the logic resources actually used by the system are addressed. This makes our fault model much more accurate than the classical stuck-at fault model. The tool relies on the SAL specification language for the modeling of netlists, and on the SAL model checker for the proof of the untestability of faults. Results from the application of the tool to some circuits from the ISCAS and ITC benchmarks are reported.

On-line testing of radiation-induced faults


[IE3TETC 2016]
Dario Cozzi, Sebastian Korf, Luca Cassano, Jens Hagemeyer, Andrea Domenici, Cinzia Bernardeschi, Mario Porrmann, Luca Sterpone OLT(RE)2: an On-Line on-demand Testing approach for permanent Radiation Effects in REconfigurable systems , IEEE Transactions on Emerging Topics in Computing, vol. PP, 2016. [ bib |  DOI |  http ]

abstract  Reconfigurable systems gained great interest in a wide range of application fields, including aerospace, where electronic devices are exposed to a very harsh working environment. Commercial SRAM-based FPGA devices represent an extremely interesting hardware platform for this kind of systems since they combine low cost with the possibility to utilize state-of-the-art processing power as well as the flexibility of reconfigurable hardware. In this paper we present OLT(RE)2: an on-line on-demand approach to test permanent faults induced by radiation in reconfigurable systems used in space missions. The proposed approach relies on a test circuit and on custom place-and-route algorithms. OLT(RE)2 exploits partial dynamic reconfigurability offered by today‚Äôs SRAM-based FPGAs to place the test circuits at run-time. The goal of OLT(RE)2 is to test unprogrammed areas of the FPGA before using them, thus preventing functional modules of the reconfigurable system to be placed on areas with faulty resources. Experimental results have shown that (i) it is possible to generate, place and route the test circuits needed to detect on average more than 99 % of the physical wires and on average about 97 % of the programmable interconnection points of an arbitrary large region of the FPGA in a reasonable time and that (ii) it is possible to download and run the whole test suite on the target device without interfering with the normal functioning of the system.


A short overview of the above activities, applied to FPGAs, is found in this paper:
[AHS 2013]
Cinzia Bernardeschi, Luca Cassano, and Andrea Domenici. Formal approaches to SEU testing in FPGAs. In 2013 NASA/ESA Conference on Adaptive Hardware and Systems (AHS-2013), Torino, Italy, 2013. [ bib | DOI ]

abstract  Various formal approaches can be used to study FPGA-based systems in relationships to faults, in particular to SEUs. Formal approaches, such as high-order logic, model checking, or Stochastic Activity Networks, have been used for fault simulation, analysis of (un)testability, and test pattern generation. This paper reports on experiences and future developments related to soft errors in the configuration memory of SRAM-based devices, which are of particular interest for reconfigurable systems.

A survey on SRAM-based FPGA development methods:

[JCST 2015]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici. SRAM-based FPGA Systems for Safety-Critical Applications: A Survey on Design Standards and Proposed Methodologies. Journal of computer science and technology vol. 30, no. 2, pp. 373-390, March 2014. [ bib |  DOI |  draft ]

abstract  As the ASIC design cost becomes affordable only for very large scale productions, the FPGA technology is currently becoming the leading technology for those applications that require a small scale production. FPGAs can be considered as a technology crossing between hardware and software. Only a small number of standards for the design of safety-critical systems give guidelines and recommendations that take the peculiarities of the FPGA technology into consideration. The main contribution of this paper is an overview of the existing design standards that regulate the design and verification of FPGA-based systems in safety-critical application fields. Moreover, the paper proposes a survey of significant published research proposals and existing industrial guidelines about the topic, and collects and reports about some lessons learned from industrial and research projects involving the use of FPGA devices.

Teaching material