{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:08:39Z","timestamp":1750306119567,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,7,20]],"date-time":"2017-07-20T00:00:00Z","timestamp":1500508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Paderborn Center for Parallel Computing"},{"name":"German Research Foundation (DFG) within the Collaborative Research Center \u201cOn-The_Fly Computing\u201d","award":["SFB 901"],"award-info":[{"award-number":["SFB 901"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2017,10,31]]},"abstract":"<jats:p>Proof-carrying hardware (PCH) is a principle for achieving safety for dynamically reconfigurable hardware systems. The producer of a hardware module spends huge effort when creating a proof for a safety policy. The proof is then transferred as a certificate together with the configuration bitstream to the consumer of the hardware module, who can quickly verify the given proof. Previous work utilized SAT solvers and resolution traces to set up a PCH technology and corresponding tool flows. In this article, we present a novel technology for PCH based on inductive invariants. For sequential circuits, our approach is fundamentally stronger than the previous SAT-based one since we avoid the limitations of bounded unrolling. We contrast our technology to existing ones and show that it fits into previously proposed tool flows. We conduct experiments with four categories of benchmark circuits and report consumer and producer runtime and peak memory consumption, as well as the size of the certificates and the distribution of the workload between producer and consumer. Experiments clearly show that our new induction-based technology is superior for sequential circuits, whereas the previous SAT-based technology is the better choice for combinational circuits.<\/jats:p>","DOI":"10.1145\/3054743","type":"journal-article","created":{"date-parts":[[2017,7,20]],"date-time":"2017-07-20T17:51:24Z","timestamp":1500573084000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Proof-Carrying Hardware via Inductive Invariants"],"prefix":"10.1145","volume":"22","author":[{"given":"Tobias","family":"Isenberg","sequence":"first","affiliation":[{"name":"Paderborn University, Paderborn, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Platzner","sequence":"additional","affiliation":[{"name":"Paderborn University, Paderborn, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[{"name":"Paderborn University, Paderborn, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Wiersema","sequence":"additional","affiliation":[{"name":"Paderborn University, Paderborn, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,7,20]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32275-7_25"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_20"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/DISCEX.2003.1194942"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_22"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0182-5"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ReConFig.2009.31"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1155\/2010\/180242"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 2011 Conference on Formal Methods in Computer-Aided Design (FMCAD\u201911)","author":"Een Niklas","year":"2011","unstructured":"Niklas Een , Alan Mishchenko , and Robert Brayton . 2011 a. Efficient implementation of property directed reachability . In Proceedings of the 2011 Conference on Formal Methods in Computer-Aided Design (FMCAD\u201911) . IEEE, Los Alamitos, CA, 125--134. Niklas Een, Alan Mishchenko, and Robert Brayton. 2011a. Efficient implementation of property directed reachability. In Proceedings of the 2011 Conference on Formal Methods in Computer-Aided Design (FMCAD\u201911). IEEE, Los Alamitos, CA, 125--134."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157675"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_45"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2008.05.002"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22969-0_12"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2632362.2632372"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/VTS.2012.6231062"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2013.6691208"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2011.2160627"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_2"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1997.601335"},{"key":"e_1_2_1_23_1","volume-title":"Necula and Peter Lee","author":"George","year":"1998","unstructured":"George C. Necula and Peter Lee . 1998 . Safe, untrusted agents using proof-carrying code. In Mobile Agents and Security. Lecture Notes in Computer Science, Vol. 1419 . Springer , 61--91. DOI:http:\/\/dx.doi.org\/10.1007\/ 3-540-68671-1_5 George C. Necula and Peter Lee. 1998. Safe, untrusted agents using proof-carrying code. In Mobile Agents and Security. Lecture Notes in Computer Science, Vol. 1419. Springer, 61--91. DOI:http:\/\/dx.doi.org\/10.1007\/ 3-540-68671-1_5"},{"key":"e_1_2_1_24_1","series-title":"Lecture Notes in Computer Science","volume-title":"Model Checking Software","author":"Peled Doron","unstructured":"Doron Peled and Lenore Zuck . 2001. From model checking to a temporal proof . In Model Checking Software . Lecture Notes in Computer Science , Vol. 2057 . Springer , 1--14. DOI:http:\/\/dx.doi.org\/10.1007\/ 3-540-45139-0_1 Doron Peled and Lenore Zuck. 2001. From model checking to a temporal proof. In Model Checking Software. Lecture Notes in Computer Science, Vol. 2057. Springer, 1--14. DOI:http:\/\/dx.doi.org\/10.1007\/ 3-540-45139-0_1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021015.15794.82"},{"key":"e_1_2_1_26_1","unstructured":"Martin Suda. 2013. Triggered clause pushing for IC3. arXiv:1307.4966.  Martin Suda. 2013. Triggered clause pushing for IC3. arXiv:1307.4966."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/FPT.2014.7082771"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ReCoSoC.2016.7533910"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-16214-0_32"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3054743","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3054743","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:36:43Z","timestamp":1750217803000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3054743"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,20]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,10,31]]}},"alternative-id":["10.1145\/3054743"],"URL":"https:\/\/doi.org\/10.1145\/3054743","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2017,7,20]]},"assertion":[{"value":"2016-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-07-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}