Translation Validation for PRES+ Models of Parallel Behaviours via an FSMD Equivalence Checker
详细信息 查看全文
- 作者：Soumyadip Bandyopadhyay (1) soumyadip@cse.iitkgp.ernet.in
Kunal Banerjee (1) kunal@cse.iitkgp.ernet.in
Dipankar Sarkar (1) ds@cse.iitkgp.ernet.in
Chittaranjan R. Mandal (1) chitta@cse.iitkgp.ernet.in - 关键词：Formal verification – ; Equivalence checker – ; PRES+ (Petri Net based Representation of Embedded Systems) – ; FSMD (Finite State Machine with Datapath)
- 刊名：Lecture Notes in Computer Science
- 出版年：2012
- 出版时间：2012
- 年：2012
- 卷：7373
- 期：1
- 页码：69-78
- 全文大小：239.4 KB
- 参考文献：1. Edwards, S., Lavagno, L., Lee, E.A., Sangiovanni-Vincentelli, A.: Design of embedded systems: Formal models, validation, and synthesis. Proceedings of the IEEE, pp. 366–390 (1997)
2. Cort茅s, L.A., Eles, P., Peng, Z.: Verification of embedded systems using a petri net based representation. In: ISSS 2000: Proceedings of the 13th International Symposium on System Synthesis, pp. 149–155. IEEE Computer Society, Washington, DC (2000)
3. Gupta, S., Gupta, R., Dutt, N., Nicolau, A.: Coordinated parallelizing compiler optimizations and high-level synthesis. ACM Transactions on Design Automation of Electronic Systems (TODAES) 9(4), 1–31 (2004)
4. Dos Santos, L.C.V., Jress, J.A.G.: A reordering technique for efficient code motion. In: Procs. of the 36th ACM/IEEE Design Automation Conference, DAC 1999, pp. 296–299. ACM, New York (1999)
5. Lakshminarayana, G., Raghunathan, A., Jha, N.K.: Incorporating speculative execution into scheduling of control-flow-intensive design. IEEE Transactions on CAD of ICS 19(3), 308–324 (2000)
6. Wakabayashi, K., Tanaka, H.: Global scheduling independent of control dependencies based on condition vectors. In: DAC 1992: Proceedings of the 29th ACM/IEEE Conference on Design Automation, pp. 112–115 (1992)
7. Rim, M., Fann, Y., Jain, R.: Global scheduling with code motions for high-level synthesis applications. IEEE Transactions on VLSI Systems 3(3), 379–392 (1995)
8. Gupta, S., Dutt, N., Gupta, R., Nicolau, A.: Using global code motions to improve the quality of results for high-level synthesis. IEEE Transactions on CAD of ICS 23(2), 302–312 (2004)
9. Kandemir, M., Vijaykrishnan, N., Irwin, M.J., Ye, W.: Influence of compiler optimizations on system power. IEEE Trans. Very Large Scale Integr. Syst. 9, 801–804 (2001)
10. Kandemir, M., Son, S.W., Chen, G.: An evaluation of code and data optimizations in the context of disk power reduction. In: ISLPED 2005: Proceedings of the 2005 International Symposium on Low Power Electronics and Design, pp. 209–214 (2005)
11. Kandemir, M.T.: Reducing energy consumption of multiprocessor soc architectures by exploiting memory bank locality. ACM Trans. Des. Autom. Electron. Syst. 11(2), 410–441 (2006)
12. Radhakrishnan, R., Teica, E., Vemuri, R.: Verification of Basic Block Schedules Using RTL Transformations. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 173–178. Springer, Heidelberg (2001)
13. Eveking, H., Hinrichsen, H., Ritter, G.: Automatic verification of scheduling results in high-level synthesis. In: Proceedings of the Conference on Design, Automation and Test in Europe, DATE 1999, pp. 260–265. ACM, New York (1999)
14. Kim, Y., Kopuri, S., Mansouri, N.: Automated formal verification of scheduling process using finite state machines with datapath (fsmd). In: Proceedings of the 5th International Symposium on Quality Electronic Design, ISQED 2004, pp. 110–115. IEEE Computer Society, Washington, DC (2004)
15. Tristan, J.-B., Leroy, X.: Verified validation of lazy code motion. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, pp. 316–326. ACM, New York (2009)
16. Kim, Y., Mansouri, N.: Automated formal verification of scheduling with speculative code motions. In: Proceedings of the 18th ACM Great Lakes Symposium on VLSI, GLSVLSI 2008, pp. 95–100. ACM, New York (2008)
17. Kundu, S., Lerner, S., Gupta, R.: Validating High-Level Synthesis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 459–472. Springer, Heidelberg (2008)
18. Karfa, C., Sarkar, D., Mandal, C., Reade, C.: Hand-in-hand verification of high-level synthesis. In: GLSVLSI 2007: Proceedings of the 17th ACM Great Lakes Symposium on VLSI, pp. 429–434. ACM, New York (2007)
19. Karfa, C., Sarkar, D., Mandal, C., Kumar, P.: An equivalence-checking method for scheduling verification in high-level synthesis. IEEE Trans. on CAD of Integrated Circuits and Systems 27(3), 556–569 (2008)
20. Kim, Y., Kopuri, S., Mansouri, N.: Automated formal verification of scheduling process using finite state machines with datapath (fsmd). In: Proceedings of the 5th International Symposium on Quality Electronic Design, ISQED 2004, pp. 110–115. IEEE Computer Society, Washington, DC (2004)
21. Bandyopadhyay, S.: Equivalence checking in embedded systems design verification using pres+ model. CoRR, abs/1010.4953 (2010)
22. Panda, P.R., Dutt, N.D.: 1995 high level synthesis design repository. In: Proceedings of the 8th International Symposium on System Synthesis, ISSS 1995, pp. 170–174 (1995)
23. Gajski, D.D., Dutt, N.D., Wu, A.C.-H., Lin, S.Y.-L.: High-level synthesis: introduction to chip and system design. Kluwer Academic Publishers, Norwell (1992)
24. Gupta, S., Dutt, N., Gupta, R., Nicolau, A.: Spark: a high-level synthesis framework for applying parallelizing compiler transformations. In: Proc. of Int. Conf. on VLSI Design, pp. 461–466. IEEE Computer Society, Washington, DC (2003)
25. Alizadeh, B., Fujita, M.: Automatic Merge-Point Detection for Sequential Equivalence Checking of System-Level and RTL Descriptions. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 129–144. Springer, Heidelberg (2007) - 作者单位：1. Dept. of Computer Science and Engineering, Indian Institute of Technology Kharagpur, India
- ISSN：1611-3349
文摘
Behavioural equivalence checking of the refinements of the input behaviours taking place at various phases of synthesis of embedded systems or VLSI circuits is a well pursued field. Although extensive literature on equivalence checking of sequential behaviours exists, similar treatments for parallel behaviours are rare mainly because of all the possible execution scenarios inherent in them. Here, we propose a translation algorithm from a parallel behaviour, represented by an untimed PRES+ model, to a sequential behaviour, represented by an FSMD model. Several equivalence checkers for FSMD models already exist for various code based transformation techniques. We have satisfactorily performed equivalence checking of some high level synthesis benchmarks represented by untimed PRES+ models by first translating them into FSMD models using our algorithm and subsequently feeding them to one such FSMD equivalence checker.