access icon openaccess Verification of parallelising transformations of KPN models

Loading full text...

Full text loading...

/deliver/fulltext/iet-cps/4/3/IET-CPS.2018.5008.html;jsessionid=sa7vtwl9ydat.x-iet-live-01?itemId=%2fcontent%2fjournals%2f10.1049%2fiet-cps.2018.5008&mimeType=html&fmt=ahah

Inspec keywords: system-on-chip; signal processing; multiprocessing systems; graph theory; parallel processing; formal verification

Other keywords: verification frameworks; sequential behaviour; KPN behaviour; signal processing applications; Kahn process networks; array data dependence graphs; KPN models; ADDG construction method; verification problem; heterogeneous multiprocessor systems

Subjects: System-on-chip; Multiprocessing systems; System-on-chip; Formal methods; Signal processing and detection; Combinatorial mathematics; Digital signal processing; Combinatorial mathematics

References

    1. 1)
      • 12. Meijer, S., Nikolov, H., Stefanov, T.: ‘On compile-time evaluation of process partitioning transformations for kahn process networks’. CODES-ISSS'09, Grenoble, France, 2009, pp. 3140.
    2. 2)
      • 13. Meijer, S., Nikolov, H., Stefanov, T.: ‘Throughput modeling to evaluate process merging transformations in polyhedral process networks’. Proc. of Int. Conf. Design, Automation and Test in Europe (DATE'10), Dresden, Germany, 2010, pp. 747752.
    3. 3)
      • 45. Jiang, B., Deprettere, E., Kienhuis, B.: ‘Hierarchical run time deadlock detection in process networks’. IEEE Workshop on Signal Processing Systems, Washington DC, USA, 2008, pp. 239244.
    4. 4)
      • 10. Davare, A., Zhu, Q., Sangiovanni-Vincentelli, A.: ‘A platform-based design flow for kahn process networks’. Technical Report 2006-30, UC Berkeley, March 2006.
    5. 5)
      • 28. Holzmann, G.J.: ‘The model checker spin’, IEEE Trans. Softw. Eng., 1997, 23, pp. 279295.
    6. 6)
      • 48. Oppen, D.C.: ‘A 222pn upper bound on the complexity of presburger arithmetic’, J. Comput. Syst. Sci., 1978, 16, (3), pp. 323332.
    7. 7)
      • 36. Strehl, K., Thiele, L.: ‘Interval diagrams for efficient symbolic verification of process networks’, IEEE Trans. CAD ICS, 2000, 19, (8), pp. 939956.
    8. 8)
      • 39. Kienhuis, B., Rijpkema, E., Deprettere, E.F.: ‘Compaan: deriving process networks from matlab for embedded signal processing architectures’. CODES'00, San Diego, CA, USA, 2000, pp. 1317.
    9. 9)
      • 1. Horowitz, M., Indermaur, T., Gonzalez, R.: ‘Low-power digital design’. IEEE Symp. on Low Power Electronics, San Diego, CA, USA, 1994, pp. 811.
    10. 10)
      • 26. Clarke, E.M., Emerson, E.A.: ‘Design and synthesis of synchronization skeletons using branching-time temporal logic’. Logic of Programs, Workshop, Berlin, Heidelberg, 1982, pp. 5271.
    11. 11)
      • 27. Queille, J.-P., Sifakis, J.: ‘Specification and verification of concurrent systems in cesar’. Proc. of the 5th Colloquium on Int. Symp. on Programming, London, UK, 1982, pp. 337351.
    12. 12)
      • 24. Park, D.: ‘Concurrency and automata on infinite sequences’. Proc. of the 5th GI-Conf. on Theoretical Computer Science, London, UK, 1981, pp. 167183.
    13. 13)
      • 9. Nikolov, H., Stefanov, T., Deprettere, E.: ‘Systematic and automated multiprocessor system design, programming, and implementation’, IEEE TCAD ICS, 2008, 27, (3), pp. 542555.
    14. 14)
      • 17. Karfa, C., Banerjee, K., Sarkar, D., et al: ‘Verification of loop and arithmetic transformations of array-intensive behaviors’, IEEE Trans. CAD ICS, 2013, 32, (11), pp. 17871800.
    15. 15)
      • 4. Kahn, G.: ‘The semantics of a simple language for parallel programming’. Proc. of IFIP Congress, Stockholm, Sweden, 1974, pp. 471475.
    16. 16)
      • 7. Daedalus, 2008. Available at http://daedalus.liacs.nl/Site/Daedalus home.html.
    17. 17)
      • 3. Turjan, A., Kienhuis, B., Deprettere, E.: ‘Translating affine nested-loop programs to process networks’. CASES'04, Washington DC, USA, 2004, pp. 220229.
    18. 18)
      • 43. Kelly, W., Rosser, E., Pugh, B., et al: ‘The omega calculator and library’, version 2.1, 2008. Available at http://www.cs.umd.edu/projects/omega/.
    19. 19)
      • 21. Hoare, C.A.R.: ‘Communicating sequential processes’, Commun. ACM, 1978, 21, (8), pp. 666677.
    20. 20)
      • 29. McMillan, K.L.: ‘Symbolic model checking’ (Kluwer Academic Publishers, Norwell, MA, USA, 1993).
    21. 21)
      • 35. Abadi, M., Lamport, L.: ‘Conjoining specifications’, ACM Trans. Program. Lang. Syst., 1995, 17, (3), pp. 507535.
    22. 22)
      • 37. Raudvere, T., Sander, I., Jantsch, A.: ‘Application and verification of local nonsemantic-preserving transformations in system design’, IEEE Trans. CAD ICS, 2008, 27, (6), pp. 10911103.
    23. 23)
      • 47. Parks, T.M.: ‘Bounded scheduling of process networks’. PhD thesis, EECS Department, University of California, Berkeley, 1995.
    24. 24)
      • 23. Hennessy, M., Milner, R.: ‘On observing nondeterminism and concurrency’. Proc. of the 7th Colloquium on Automata, Languages and Programming, Berlin, Heidelberg, 1980, pp. 299309.
    25. 25)
      • 19. Kumar, A., Fernando, S., Ha, Y., et al: ‘Multiprocessor systems synthesis for multiple use-cases of multiple applications on fpga’, ACM Trans. Des. Autom. Electron. Syst., 2008, 13, (3), pp. 40:140:27.
    26. 26)
      • 42. The Yices SMT Solver. Available at http://yices.csl.sri.com/.
    27. 27)
      • 6. Artemis, 2005. Available at http://ce.et.tudelft.nl/artemis/.
    28. 28)
      • 33. Dams, D., Gerth, R., Grumberg, O.: ‘Abstract interpretation of reactive systems’, ACM Trans. Program. Lang. Syst., 1997, 19, (2), pp. 253291.
    29. 29)
      • 8. Metropilis, 2008. http://embedded.eecs.berkeley.edu/metropolis/.
    30. 30)
      • 22. Bergstra, J., Klop, J.: ‘Process algebra for synchronous communication’, Inf. Control, 1984, 60, (1), pp. 109137.
    31. 31)
      • 34. Clarke, E.M., Enders, R., Filkorn, T., et al: ‘Exploiting symmetry in temporal logic model checking’, Form. Methods Syst. Des., 1996, 9, (1–2), pp. 77104.
    32. 32)
      • 46. Olson, A., Evans, B.: ‘Deadlock detection for distributed process networks’. IEEE Int. Conf. on Acoustics, Speech, and Signal Processing, Philadelphia, PA, USA, 2005, vol. 5, pp. v/73v/76.
    33. 33)
      • 41. lp_solve, 2010. http://lpsolve.sourceforge.net/5.5/.
    34. 34)
      • 25. Pnueli, A.: ‘The temporal logic of programs’. 18th Annual Symp. on Foundations of Computer Science (sfcs 1977), San Diego, California, USA, October 1977, pp. 4657.
    35. 35)
      • 15. Kundu, S., Lerner, S., Gupta, R.: ‘Translation validation of high-level synthesis’, IEEE Trans. CAD ICS, 2010, 29, (4), pp. 566579.
    36. 36)
      • 31. Burch, J.R., Clarke, E.M., Long, D.E., et al: ‘Symbolic model checking for sequential circuit verification’, IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., 1994, 13, (4), pp. 401424.
    37. 37)
      • 14. Kundu, S., Tatlock, Z., Lerner, S.: ‘Proving optimizations correct using parameterized program equivalence’. PLDI ‘09, Dublin, Ireland, 2009, pp. 327337.
    38. 38)
      • 30. Fernandez, J.-C., Garavel, H., Kerbrat, A., et al: ‘Cadp – a protocol validation and verification toolbox’. Proc. of the 8th Int. Conf. on Computer Aided Verification, CAV ‘96, London, UK, 1996, pp. 437440.
    39. 39)
      • 16. Shashidhar, K.C.: ‘Efficient automatic verification of loop and data-flow transformations by functional equivalence checking’. PhD thesis, Department of Computer Science, Katholieke Universiteit Leuven, Belgium, 2008.
    40. 40)
      • 44. Cheung, E., Chen, X., Hsieh, H., et al: ‘Runtime deadlock analysis for system level design’, Des. Autom. Embedded Syst., 2009, 13, pp. 287310.
    41. 41)
      • 11. Fei, Y., Ravi, S., Raghunathan, A., et al: ‘Energy-optimizing source code transformations for operating system-driven embedded software’, Trans. Embedded Comput. Syst., 2007, 7, (1), pp. 126.
    42. 42)
      • 2. Turjan, A.: ‘Compiling nested loop programs to process networks’. PhD thesis, Leiden University, 2007.
    43. 43)
      • 18. Karfa, C., Sarkar, D., Mandal, C.: ‘Verification of KPN level transformations’. 26th Int. Conf. on VLSI Design, Pune, India, 2013, pp. 338343.
    44. 44)
      • 38. Chen, X., Hsieh, H., Balarin, F., et al: ‘Formal verification for embedded system designs’, Des. Autom. Embedded Syst., 2003, 8, pp. 139153.
    45. 45)
      • 40. Manna, Z.: ‘Mathematical theory of computation’ (McGraw-Hill Kogakusha, Tokyo, 1974).
    46. 46)
      • 32. Godefroid, P.: ‘Using partial orders to improve automatic verification methods’. Proc. of the 2Nd Int. Workshop on Computer Aided Verification, CAV ‘90, Berlin, Heidelberg, 1991, pp. 176185.
    47. 47)
      • 5. Compaan, 2000.
    48. 48)
      • 20. Milner, R.: ‘A calculus of communicating systems’ (Springer-Verlag, Berlin, Heidelberg, 1982).
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cps.2018.5008
Loading

Related content

content/journals/10.1049/iet-cps.2018.5008
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading