{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:26Z","timestamp":1776305246987,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":12,"publisher":"ACM","license":[{"start":{"date-parts":[[2006,4,30]],"date-time":"2006-04-30T00:00:00Z","timestamp":1146355200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2006,4,30]]},"DOI":"10.1145\/1127908.1127920","type":"proceedings-article","created":{"date-parts":[[2006,5,8]],"date-time":"2006-05-08T21:40:43Z","timestamp":1147124443000},"page":"43-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["HW\/SW co-verification of embedded systems using bounded model checking"],"prefix":"10.1145","author":[{"given":"Daniel","family":"Gro\u03b2e","sequence":"first","affiliation":[{"name":"University of Bremen, Bremen, Germany"}]},{"given":"Ulrich","family":"K\u00fchne","sequence":"additional","affiliation":[{"name":"University of Bremen, Bremen, Germany"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[{"name":"University of Bremen, Bremen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2006,4,30]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Accellera Property Specification Language Reference Manual version 1.1. http:\/\/www.pslsugar.org 2005.]]  Accellera Property Specification Language Reference Manual version 1.1. http:\/\/www.pslsugar.org 2005.]]"},{"key":"e_1_3_2_1_2_1","volume-title":"Pearson Education Deutschland","author":"Becker B.","year":"2005","unstructured":"B. Becker , R. Drechsler , and P. Molitor . Technische Informatik --- Eine Einf\u00fchrung . Pearson Education Deutschland , 2005 .]] B. Becker, R. Drechsler, and P. Molitor. Technische Informatik --- Eine Einf\u00fchrung. Pearson Education Deutschland, 2005.]]"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_3_2_1_4_1","series-title":"LNCS","first-page":"372","volume-title":"Int'l Conf. on Formal Methods in CAD","author":"Bjesse P.","year":"2000","unstructured":"P. Bjesse and K. Claessen . SAT-based verification without state space traversal . In Int'l Conf. on Formal Methods in CAD , volume 1954 of LNCS , pages 372 -- 389 . Springer , 2000 .]] P. Bjesse and K. Claessen. SAT-based verification without state space traversal. In Int'l Conf. on Formal Methods in CAD, volume 1954 of LNCS, pages 372--389. Springer, 2000.]]"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/RSP.2005.46"},{"key":"e_1_3_2_1_6_1","first-page":"4167","volume-title":"IEEE International Symposium on Circuits and Systems","author":"Gro\u03b2e D.","year":"2005","unstructured":"D. Gro\u03b2e and R. Drechsler . CheckSyC: An efficient property checker for RTL SystemC designs . In IEEE International Symposium on Circuits and Systems , pages 4167 -- 4170 , 2005 .]] D. Gro\u03b2e and R. Drechsler. CheckSyC: An efficient property checker for RTL SystemC designs. In IEEE International Symposium on Circuits and Systems, pages 4167--4170, 2005.]]"},{"key":"e_1_3_2_1_7_1","volume-title":"ITG\/GI\/GMM-Workshop \"Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen\"","author":"Gro\u03b2e D.","year":"2005","unstructured":"D. Gro\u03b2e , U. K\u00fchne , C. Genz , F. Schmiedle , B. Becker , R. Drechsler , and P. Molitor . Modellierung eines Mikroprozessors in SystemC . In ITG\/GI\/GMM-Workshop \"Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen\" , 2005 .]] D. Gro\u03b2e, U. K\u00fchne, C. Genz, F. Schmiedle, B. Becker, R. Drechsler, and P. Molitor. Modellierung eines Mikroprozessors in SystemC. In ITG\/GI\/GMM-Workshop \"Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen\", 2005.]]"},{"key":"e_1_3_2_1_8_1","volume-title":"System Design with SystemC","author":"Gr\u00f6tker T.","year":"2002","unstructured":"T. Gr\u00f6tker , S. Liao , G. Martin , and S. Swan . System Design with SystemC . Kluwer Academic Publishers , 2002 .]] T. Gr\u00f6tker, S. Liao, G. Martin, and S. Swan. System Design with SystemC. Kluwer Academic Publishers, 2002.]]"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_10_1","series-title":"LNCS","first-page":"108","volume-title":"Int'l Conf. on Formal Methods in CAD","author":"Sheeran M.","year":"2000","unstructured":"M. Sheeran , S. Singh , and G. St\u00e5lmarck . Checking safety properties using induction and a SAT-solver . In Int'l Conf. on Formal Methods in CAD , volume 1954 of LNCS , pages 108 -- 125 . Springer , 2000 .]] M. Sheeran, S. Singh, and G. St\u00e5lmarck. Checking safety properties using induction and a SAT-solver. In Int'l Conf. on Formal Methods in CAD, volume 1954 of LNCS, pages 108--125. Springer, 2000.]]"},{"key":"e_1_3_2_1_11_1","unstructured":"Synopsys Inc. CoWare Inc. and Frontier Design Inc. http:\/\/www.systemc.org. Functional Specification for SystemC 2.0.]]  Synopsys Inc. CoWare Inc. and Frontier Design Inc. http:\/\/www.systemc.org. Functional Specification for SystemC 2.0.]]"},{"key":"e_1_3_2_1_12_1","first-page":"162","volume":"1","author":"Winkelmann K.","year":"2004","unstructured":"K. Winkelmann , H.-J. Trylus , D. Stoffel , and G. Fey . Cost-efficient block verification for a UMTS up-link chip-rate coprocessor. In Design, Automation and Test in Europe , volume 1 , pages 162 -- 167 , 2004 .]] K. Winkelmann, H.-J. Trylus, D. Stoffel, and G. Fey. Cost-efficient block verification for a UMTS up-link chip-rate coprocessor. In Design, Automation and Test in Europe, volume 1, pages 162--167, 2004.]]","journal-title":"In Design, Automation and Test in Europe"}],"event":{"name":"GLSVLSI06: Great Lakes Symposium on VLSI 2006","location":"Philadelphia PA USA","acronym":"GLSVLSI06","sponsor":["ACM Association for Computing Machinery","SIGDA ACM Special Interest Group on Design Automation"]},"container-title":["Proceedings of the 16th ACM Great Lakes symposium on VLSI"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1127908.1127920","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1127908.1127920","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:20Z","timestamp":1750259180000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1127908.1127920"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,4,30]]},"references-count":12,"alternative-id":["10.1145\/1127908.1127920","10.1145\/1127908"],"URL":"https:\/\/doi.org\/10.1145\/1127908.1127920","relation":{},"subject":[],"published":{"date-parts":[[2006,4,30]]},"assertion":[{"value":"2006-04-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}