{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,8]],"date-time":"2024-04-08T07:17:12Z","timestamp":1712560632142},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2010,12]]},"abstract":"SystemC is a system-level modeling language that can be used effectively for hardware\/software co-design. Since a major goal of SystemC is to enable verification at higher levels of abstraction, the tendency is now directing to introducing formal verification approaches for SystemC. In this article, we propose an approach for formal verification of SystemC designs, and provide the semantics of SystemC using Labeled Transition Systems (LTS) for this purpose. An actor-based language, Rebeca, is used as an intermediate language. SystemC designs are mapped to Rebeca models and then Rebeca verification toolset is used to verify LTL and CTL properties. To tackle the state-space explosion, Rebeca model checkers offer some reduction policies that make them appropriate for SystemC verification. The approach also benefits from the modular verification and program slicing techniques applied on Rebeca models. To show the applicability of our approach, we verified a single-cycle MIPS design and two hardware\/software co-designs. The results show that our approach can effectively be used both in hardware and hardware\/software co-verification.<\/jats:p>","DOI":"10.1145\/1880050.1880055","type":"journal-article","created":{"date-parts":[[2011,1,5]],"date-time":"2011-01-05T16:59:17Z","timestamp":1294246757000},"page":"1-35","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Sysfier"],"prefix":"10.1145","volume":"10","author":[{"given":"Niloofar","family":"Razavi","sequence":"first","affiliation":[{"name":"University of Tehran, Tehran, Iran"}]},{"given":"Razieh","family":"Behjati","sequence":"additional","affiliation":[{"name":"University of Tehran, Tehran, Iran"}]},{"given":"Hamideh","family":"Sabouri","sequence":"additional","affiliation":[{"name":"University of Tehran, Tehran, Iran"}]},{"given":"Ehsan","family":"Khamespanah","sequence":"additional","affiliation":[{"name":"University of Tehran, Tehran, Iran"}]},{"given":"Amin","family":"Shali","sequence":"additional","affiliation":[{"name":"University of Tehran, Tehran, Iran"}]},{"given":"Marjan","family":"Sirjani","sequence":"additional","affiliation":[{"name":"University of Tehran, Tehran, Iran and Reykjavik University, Iceland"}]}],"member":"320","published-online":{"date-parts":[[2011,1,7]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 8th International Conference on Application of Concurrency to System Design. IEEE","author":"Behjati R.","unstructured":"Behjati , R. , Sabouri , H. , Razavi , N. , and Sirjani , M . 2008. An effective approach for model checking SystemC designs . In Proceedings of the 8th International Conference on Application of Concurrency to System Design. IEEE , Los Alamitos, CA. Behjati, R., Sabouri, H., Razavi, N., and Sirjani, M. 2008. An effective approach for model checking SystemC designs. In Proceedings of the 8th International Conference on Application of Concurrency to System Design. IEEE, Los Alamitos, CA."},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Black D. and Donovan J. 2004. SystemC: From the Ground Up. Springer Science+Business Media New York. Black D. and Donovan J. 2004. SystemC: From the Ground Up. Springer Science+Business Media New York.","DOI":"10.1007\/0-387-30864-4"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 25th International Conference on Software Engineering. IEEE","author":"Chaki S.","unstructured":"Chaki , S. , Clarke , E. , Groce , A. , Jha , S. , and Veith , H . 2003. Modular verification of software components in C . In Proceedings of the 25th International Conference on Software Engineering. IEEE , Los Alamitos, CA, 385--395. Chaki, S., Clarke, E., Groce, A., Jha, S., and Veith, H. 2003. Modular verification of software components in C. In Proceedings of the 25th International Conference on Software Engineering. IEEE, Los Alamitos, CA, 385--395."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/501790.501822"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the Euromicro Symposium on Digital Systems Design. IEEE","author":"Drechsler R.","unstructured":"Drechsler , R. and Grosse , D . 2002. Reachability analysis for formal verification of SystemC . In Proceedings of the Euromicro Symposium on Digital Systems Design. IEEE , Los Alamitos, CA, 337--340. Drechsler, R. and Grosse, D. 2002. Reachability analysis for formal verification of SystemC. In Proceedings of the Euromicro Symposium on Digital Systems Design. IEEE, Los Alamitos, CA, 337--340."},{"key":"e_1_2_1_6_1","volume-title":"Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics","author":"Emerson E.","unstructured":"Emerson , E. 1990. Temporal and modal logic . In J. van Leeuwen, ed., Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics . MIT Press , Cambridge, MA , 995--1072. Emerson, E. 1990. Temporal and modal logic. In J. van Leeuwen, ed., Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics. MIT Press, Cambridge, MA, 995--1072."},{"key":"e_1_2_1_7_1","unstructured":"FZI -- Microelectronic System Design. 2006. KaSCPar. www.fzi.de\/downloads\/sim\/archives\/kascpar-documentation.pdf. FZI -- Microelectronic System Design. 2006. KaSCPar. www.fzi.de\/downloads\/sim\/archives\/kascpar-documentation.pdf."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of Forum on Specification and Design Languages, 19--22","author":"Gawanmeh A.","unstructured":"Gawanmeh , A. , Habibi , A. , and Tahar , S . 2004. Enabling SystemC verification using abstract state machines . In Proceedings of Forum on Specification and Design Languages, 19--22 . Gawanmeh, A., Habibi, A., and Tahar, S. 2004. Enabling SystemC verification using abstract state machines. In Proceedings of Forum on Specification and Design Languages, 19--22."},{"key":"e_1_2_1_9_1","volume-title":"TLM Concepts and Applications for Embedded Systems","author":"Ghenassia F.","unstructured":"Ghenassia , F. , ed. 2005. Transaction-Level Modeling with SystemC , TLM Concepts and Applications for Embedded Systems . Springer , Berlin . Ghenassia, F., ed. 2005. Transaction-Level Modeling with SystemC, TLM Concepts and Applications for Embedded Systems. Springer, Berlin."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the International Symposium on Circuits and Systems. IEEE","author":"Grosse D.","unstructured":"Grosse , D. and Drechsler , R . 2003. Formal verification of LTL formulas for SystemC designs . In Proceedings of the International Symposium on Circuits and Systems. IEEE , Los Alamitos, CA, 245--248. Grosse, D. and Drechsler, R. 2003. Formal verification of LTL formulas for SystemC designs. In Proceedings of the International Symposium on Circuits and Systems. IEEE, Los Alamitos, CA, 245--248."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.01.021"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2005.863187"},{"key":"e_1_2_1_13_1","volume-title":"Proceed of the 8th International Conference on Application of Concurrency to System Design. IEEE","author":"Hojjat H.","unstructured":"Hojjat , H. , Mousavi , M. R. , and Sirjani , M . 2008. Process algebraic verification of SystemC codes . In Proceed of the 8th International Conference on Application of Concurrency to System Design. IEEE , Los Alamitos, CA. Hojjat, H., Mousavi, M. R., and Sirjani, M. 2008. Process algebraic verification of SystemC codes. In Proceed of the 8th International Conference on Application of Concurrency to System Design. IEEE, Los Alamitos, CA."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1141277.1141704"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11604655_56"},{"key":"e_1_2_1_16_1","unstructured":"Jaghoori M. Sirjani M. Mousavi M. and Movaghar A. 2007. Symmetry and partial order reduction techniques in model checking Rebeca. Tech. rep. SEN-R0704. Jaghoori M. Sirjani M. Mousavi M. and Movaghar A. 2007. Symmetry and partial order reduction techniques in model checking Rebeca. Tech. rep. SEN-R0704."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2005.1487900"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391469.1391706"},{"key":"e_1_2_1_19_1","first-page":"2","article-title":"LusSy: An open tool for the analysis of Systems-on-a-Chip at the transaction level","volume":"10","author":"Moy M.","year":"2006","unstructured":"Moy , M. , Maraninchi , F. , and Maillet-Contoz , L. 2006 . LusSy: An open tool for the analysis of Systems-on-a-Chip at the transaction level . Des. Autom. Embedded Syst. 10 , 2 - 3 , 73--104. Moy, M., Maraninchi, F., and Maillet-Contoz, L. 2006. LusSy: An open tool for the analysis of Systems-on-a-Chip at the transaction level. Des. Autom. Embedded Syst. 10, 2-3, 73--104.","journal-title":"Des. Autom. Embedded Syst."},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the Design, Automation, and Test in Europe. IEEE","author":"Mueller W.","unstructured":"Mueller , W. , Ruf , J. , Hoffmann , D. , Gerlach , J. , Kropf , T. , and Rosenstiehl , W . 2001. The simulation semantics of systemC . In Proceedings of the Design, Automation, and Test in Europe. IEEE , Los Alamitos, CA, 64--70. Mueller, W., Ruf, J., Hoffmann, D., Gerlach, J., Kropf, T., and Rosenstiehl, W. 2001. The simulation semantics of systemC. In Proceedings of the Design, Automation, and Test in Europe. IEEE, Los Alamitos, CA, 64--70."},{"key":"e_1_2_1_21_1","unstructured":"Muller W. Ruf J. and Rosenstiel W. 2003. SystemC\u2014Methodologies and Applications. Kluwer Academic Publishers Dordrecht The Netherlands 97--126. Muller W. Ruf J. and Rosenstiel W. 2003. SystemC\u2014Methodologies and Applications. Kluwer Academic Publishers Dordrecht The Netherlands 97--126."},{"key":"e_1_2_1_22_1","unstructured":"Open SystemC Initiative. 2005. IEEE 1666: SystemC Language Reference Manual. Open SystemC Initiative. http:\/\/standards.ieee.org\/getieee\/1666\/download\/1666-2005.pdf. Open SystemC Initiative. 2005. IEEE 1666: SystemC Language Reference Manual. Open SystemC Initiative. http:\/\/standards.ieee.org\/getieee\/1666\/download\/1666-2005.pdf."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1278480.1278489"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/647172.716123"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of Formal Methods and Models for Codesign. IEEE","author":"Razavi N.","unstructured":"Razavi , N. and Sirjani , M . 2006. Using Reo for formal specification and verification of system designs . In Proceedings of Formal Methods and Models for Codesign. IEEE , Los Alamitos, CA, 113--122. Razavi, N. and Sirjani, M. 2006. Using Reo for formal specification and verification of system designs. In Proceedings of Formal Methods and Models for Codesign. IEEE, Los Alamitos, CA, 113--122."},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the International Symposium on Fundamentals of Software Engineering. Springer-Verlag","author":"Razavi N.","unstructured":"Razavi , N. and Sirjani , M . 2007. Compositional semantics of system-level designs written in SystemC . In Proceedings of the International Symposium on Fundamentals of Software Engineering. Springer-Verlag , Berlin, 113--128. Razavi, N. and Sirjani, M. 2007. Compositional semantics of system-level designs written in SystemC. In Proceedings of the International Symposium on Fundamentals of Software Engineering. Springer-Verlag, Berlin, 113--128."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 5th International Workshop on Formal Aspect of Component Software. Elsevier","author":"Sabouri H.","unstructured":"Sabouri , H. and Sirjani , M . 2008. Slicing-based reductions for Rebeca . In Proceedings of the 5th International Workshop on Formal Aspect of Component Software. Elsevier , Cambridge, MA. Sabouri, H. and Sirjani, M. 2008. Slicing-based reductions for Rebeca. In Proceedings of the 5th International Workshop on Formal Aspect of Component Software. Elsevier, Cambridge, MA."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/789083.1022755"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2005.1487903"},{"key":"e_1_2_1_30_1","first-page":"1695","article-title":"Modular verification of a component-based actor language","volume":"11","author":"Sirjani M.","year":"2005","unstructured":"Sirjani , M. , de Boer , F. S. , and Movaghar , A. 2005 . Modular verification of a component-based actor language . J. Universal Comput. Sci. 11 , 10, 1695 -- 1717 . Sirjani, M., de Boer, F. S., and Movaghar, A. 2005. Modular verification of a component-based actor language. J. Universal Comput. Sci. 11, 10, 1695--1717.","journal-title":"J. Universal Comput. Sci."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/2370686.2370691"},{"key":"e_1_2_1_32_1","first-page":"1054","article-title":"Model checking, automated abstraction, and compositional verification of Rebeca models","volume":"11","author":"Sirjani M.","year":"2005","unstructured":"Sirjani , M. , Movaghar , A. , Shali , A. , and de Boer , F. S. 2005 . Model checking, automated abstraction, and compositional verification of Rebeca models . J. Universal Comput. Sci. 11 , 6, 1054 -- 1082 . Sirjani, M., Movaghar, A., Shali, A., and de Boer, F. S. 2005. Model checking, automated abstraction, and compositional verification of Rebeca models. J. Universal Comput. Sci. 11, 6, 1054--1082.","journal-title":"J. Universal Comput. Sci."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734097"},{"key":"e_1_2_1_34_1","unstructured":"SyMon: SystemC Model-checking engine technical report. http:\/\/khorshid.ece.ut.ac.ir\/_rebeca\/afra\/SyMon.pdf. SyMon: SystemC Model-checking engine technical report. http:\/\/khorshid.ece.ut.ac.ir\/_rebeca\/afra\/SyMon.pdf."},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 14th Workshop on Model Checking Software SPIN. Springer-Verlag","author":"Traulsen C.","unstructured":"Traulsen , C. , Cornet , J. , Moy , M. , and Maraninchi , F . 2007. A SystemC\/TLM semantics in Promela and its possible applications . In Proceedings of the 14th Workshop on Model Checking Software SPIN. Springer-Verlag , Berlin. Traulsen, C., Cornet, J., Moy, M., and Maraninchi, F. 2007. A SystemC\/TLM semantics in Promela and its possible applications. In Proceedings of the 14th Workshop on Model Checking Software SPIN. Springer-Verlag, Berlin."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1278480.1278527"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/800078.802557"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1880050.1880055","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T21:17:42Z","timestamp":1672348662000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1880050.1880055"}},"subtitle":["Actor-based formal verification of SystemC"],"short-title":[],"issued":{"date-parts":[[2010,12]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["10.1145\/1880050.1880055"],"URL":"http:\/\/dx.doi.org\/10.1145\/1880050.1880055","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12]]},"assertion":[{"value":"2008-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}
