access icon free Formal verification methodology for real-time Field Programmable Gate Array

A formal verification methodology for checking both functional and timing requirements of real-time digital controllers targeted at field programmable gate array technology is proposed. Timed transition systems (TTSs) are used to model both the digital controller circuit and the high-level specification requirements. Timed well-founded simulation (TWFS) refinement is used as the notion of correctness and defines what it means for an implementation TTS to satisfy a specification TTS. The primary contribution is a set of proof obligation templates (based on TWFS refinement) that account for both functional and timing requirements. The proof obligations generated using the templates can be checked using a decision procedure. One of the key ideas is the overloaded use of rank functions (that are typically used for liveness verification) for timing verification. The efficiency and scalability of the approach is demonstrated using three case studies.

Inspec keywords: formal verification; field programmable gate arrays

Other keywords: real-time field programmable gate array; proof obligation templates; timed transition systems; real-time digital controllers; timed well-founded simulation; formal verification methodology; high-level specification requirements

Subjects: Logic circuits; Logic and switching circuits; Protocols; Protocols

References

    1. 1)
      • 1. Chen, Y., Dinavahi, V.: ‘Multi-FPGA digital hardware design for detailed large-scale real-time electromagnetic transient simulation of power systems’, IET Gener. Trans. Distrib., 2013, 7, pp. 451463.
    2. 2)
      • 14. Shuja, S., Srinivasan, S.K., Jabeen, S., et al: ‘A formal verification methodology for DDD mode pacemaker control programs’, J. Electric. Comput. Eng., 2015, 2015, p. 57.
    3. 3)
      • 7. Sanyal, A., Chakrabarty, K., Yilmaz, M., et al: ‘RT-level design-for-testability and expansion of functional test sequences for enhanced defect coverage’. Proc. of IEEE Int. Test Conf., 2010, pp. 110.
    4. 4)
      • 15. Mangassarian, H., Le, B., Veneris, A.: ‘Debugging RTL using structural dominance’, IEEE Trans. Comput. Aided Des. Integr. Circ. Syst., 2014, 33, pp. 153166.
    5. 5)
      • 21. Manolios, P.: ‘Mechanical verification of reactive systems’. PhD thesis, University of Texas, 2001.
    6. 6)
      • 23. Jabeen, S., Srinivasan, S.K., Shuja, S., et al: ‘A formal verification methodology for FPGA-based stepper motor control’, IEEE Embedded Syst. Lett., 2015, 7, pp. 8588.
    7. 7)
      • 9. Larsen, K.G., Pettersson, P., Yi, W.: ‘UPPAAL in a nutshell’, Int. J. Softw. Tools Technol. Transfer, 1997, 1, pp. 134152.
    8. 8)
      • 5. Hartley, E.N., Jerez, J.L., Suardi, A., et al: ‘Predictive control using an FPGA with application to aircraft control’, IEEE Trans. Control Syst. Technol., 2014, 22, pp. 10061017.
    9. 9)
      • 12. Robertson, I., Irvine, J., Lysaght, P., et al: ‘Timing verification of dynamically reconfigurable logic for the Xilinx Virtex FPGA series’. Proc. 2002 ACM/SIGDA Tenth Int. Symp. Field-Programmable Gate Arrays, 2002, pp. 127135.
    10. 10)
      • 10. Yovine, S.: ‘Kronos: a verification tool for real-time systems’, Int. J. Softw. Tools Technol. Transfer, 1997, 1, pp. 123133.
    11. 11)
      • 17. David, A., Larsen, K.G., Legay, A., et al: ‘Timed I/O automata: a complete specification theory for real-time systems’. Proc. 13th ACM Int. Conf. Hybrid Systems: Computation and Control, 2010, pp. 91100.
    12. 12)
      • 6. Jagadeesh, G.R., Srikanthan, T., Lim, C.M.: ‘Field programmable gate array-based acceleration of shortest-path computation’, IET Comput. Digit. Tech., 2011, 5, pp. 231237.
    13. 13)
      • 22. Dubasi, M.A.L., Sudarshan, S.K., Wijayasekara, V.: ‘Timed refinement for verification of real-time object code programs’. Working Conf. Verified Software: Theories, Tools, and Experiments, 2014, pp. 252269.
    14. 14)
      • 13. Simulation Tool, Available at http://www.utdallas.edu/poras/courses/ee3320/xilinx/upenn/FoundationtutorialFunctionalandTimingsimulation.htm, accessed 17 March 2017.
    15. 15)
      • 8. Bareisa, E., Jusas, V., Motiejunas, K.: ‘Path delay test generation at functional level’, IET Comput. Digit. Tech., 2015, 9, pp. 135141.
    16. 16)
      • 24. Boston Scientific: ‘Pacemaker system specification’ (Boston Scientific, 2007).
    17. 17)
      • 18. Boudjadar, A., Bodeveix, J.P., Filali, M.: ‘Compositional refinement for real-time systems with priorities’. 19th Int. Symp. Temporal Representation and Reasoning, 2012, pp. 5764.
    18. 18)
      • 3. Di Carlo, S., Gambardella, G., Prinetto, P., et al: ‘SA-FEMIP: a self-adaptive features extractor and matcher IP-core based on partially reconfigurable FPGAs for space applications’, IEEE Trans. VLSI Syst., 2015, 23, pp. 21982208.
    19. 19)
      • 19. De Moura, L., Bjørner, N.: ‘Satisfiability modulo theories: introduction and applications’, Commun. ACM, 2011, 54, pp. 6977.
    20. 20)
      • 20. De Moura, L., Bjørner, N.: ‘Z3: An efficient SMT solver’. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2008, pp. 337340.
    21. 21)
      • 2. Milivojevic, N., Krishnamurthy, M., Gurkaynak, Y., et al: ‘Analysis of FPGA-based control of brushless DC motors and generators using digital PWM technique’, IEEE Trans. Ind. Electron., 2012, 59, pp. 343351.
    22. 22)
      • 11. Godskesen, J.C., Larsen, K.G., Skou, A.: ‘Automatic verification of real-timed systems using Epsilon’, ‘Protocol specification, testing and verification XIV’ (Springer, USA, 1995), pp. 323330.
    23. 23)
      • 4. Kharchenko, V., Kovalenko, A., Siora, O., et al: ‘Security assessment of FPGA-based safety-critical systems: US NRC requirements context’. IEEE Int. Conf. Information and Digital Technologies (IDT), Zilina, 2015, pp. 132138.
    24. 24)
      • 16. Urdahl, J., Stoffel, D., Kunz, W.: ‘Path predicate abstraction for sound system-level models of RT-level circuit designs’, IEEE Trans. Comput. Aided Des. Integr. Circ. Syst., 2014, 33, pp. 291304.
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cdt.2016.0189
Loading

Related content

content/journals/10.1049/iet-cdt.2016.0189
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading