{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:52:14Z","timestamp":1750308734944,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2012,10,1]],"date-time":"2012-10-01T00:00:00Z","timestamp":1349049600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["2008-TJ-1835"],"award-info":[{"award-number":["2008-TJ-1835"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2012,10]]},"abstract":"<jats:p>The verification community anticipates the adoption of assertions in the Analog and Mixed-Signal (AMS) domain in the near future. Several questions need to be answered before AMS assertions are brought into practice, such as: (a) How will the languages for AMS assertions be different from the ones in the digital domain? (b) Does the analog simulator have to be assertion aware? (c) If so, then how and where on the time line will the AMS assertion checker synchronize with the analog simulator? and (d) What will be the performance penalty for monitoring AMS assertions accurately over analog simulation? This article attempts to answer these questions through theoretical analysis and empirical results obtained from industrial test cases. We study logics which extend Linear Temporal Logic (LTL) with predicates over real variables, and show that further extensions allowing the binding of real-valued variables across time makes the logic undecidable. We present a toolkit which can integrate with existing AMS simulators for checking AMS assertions on practical designs. We study the problem of synchronizing the AMS simulator with the AMS assertion checker and demonstrate the performance penalty of different synchronization options.<\/jats:p>","DOI":"10.1145\/2348839.2348842","type":"journal-article","created":{"date-parts":[[2012,10,18]],"date-time":"2012-10-18T13:48:27Z","timestamp":1350568107000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Synchronizing AMS Assertions with AMS Simulation"],"prefix":"10.1145","volume":"17","author":[{"given":"Subhankar","family":"Mukherjee","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Kharagpur"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pallab","family":"Dasgupta","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kharagpur"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Siddhartha","family":"Mukhopadhyay","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kharagpur"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Scott","family":"Little","sequence":"additional","affiliation":[{"name":"Freescale Semiconductor"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Havlicek","sequence":"additional","affiliation":[{"name":"Freescale Semiconductor"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Srikanth","family":"Chandrasekaran","sequence":"additional","affiliation":[{"name":"Freescale Semiconductor"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1025"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_21"},{"volume-title":"A Roadmap for Formal Property Verification","author":"Dasgupta P.","key":"e_1_2_1_5_1","unstructured":"Dasgupta , P. 2006. A Roadmap for Formal Property Verification . Springer . Dasgupta, P. 2006. A Roadmap for Formal Property Verification. Springer."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1255456.1255468"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888256"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"volume-title":"Proceedings of the 1st ACM and IEEE International Conference on Formal Methods and Models for Co-Design. IEEE Computer Society, 163","author":"Huang J.","key":"e_1_2_1_9_1","unstructured":"Huang , J. , Voeten , J. , and Geilen , M . 2003. Real-Time property preservation in approximations of timed systems . In Proceedings of the 1st ACM and IEEE International Conference on Formal Methods and Models for Co-Design. IEEE Computer Society, 163 . Huang, J., Voeten, J., and Geilen, M. 2003. Real-Time property preservation in approximations of timed systems. In Proceedings of the 1st ACM and IEEE International Conference on Formal Methods and Models for Co-Design. IEEE Computer Society, 163."},{"key":"e_1_2_1_10_1","unstructured":"IEEE Std 1800-2009. 2010. IEEE standard for system verilog: Unified hardware design specification and verification language. http:\/\/ieeexplore.ieee.org\/xpl\/login.jsp?tp=&arnumber=5354441&url=http&percnt;&url=http&percnt;&percnt;3A&percnt;2Fieeexplore.ieee.org&percnt;2Fxpls&percnt;2Fabs_all.jsp&percnt;3Farnumber&percnt;3D5354441. IEEE Std 1800-2009 . 2010. IEEE standard for system verilog: Unified hardware design specification and verification language. http:\/\/ieeexplore.ieee.org\/xpl\/login.jsp?tp=&arnumber=5354441&url=http&percnt;&url=http&percnt;&percnt;3A&percnt;2Fieeexplore.ieee.org&percnt;2Fxpls&percnt;2Fabs_all.jsp&percnt;3Farnumber&percnt;3D5354441."},{"key":"e_1_2_1_11_1","unstructured":"IEEE Std 1850-2010. 2010. IEEE standard for property Specification language (PSL). http:\/\/standards.ieee.org\/findstds\/standard\/1850-2010.html. IEEE Std 1850-2010 . 2010. IEEE standard for property Specification language (PSL). http:\/\/standards.ieee.org\/findstds\/standard\/1850-2010.html."},{"volume-title":"Proceedings of the 14th Workshop on Synthesis and System Integration of Mixed Information Technologies. 507--514","author":"Jesser A.","key":"e_1_2_1_12_1","unstructured":"Jesser , A. , L\u00e4mmermann , S. , Pacholik , A. , Weiss , R. , Ruf , J. , Fengler , W. , Hedrich , L. , Kropf , T. , and Rosenstiel , W . 2007. Analog simulation meets digital verification - A formal assertion approach for mixed-signal verification . In Proceedings of the 14th Workshop on Synthesis and System Integration of Mixed Information Technologies. 507--514 . Jesser, A., L\u00e4mmermann, S., Pacholik, A., Weiss, R., Ruf, J., Fengler, W., Hedrich, L., Kropf, T., and Rosenstiel, W. 2007. Analog simulation meets digital verification - A formal assertion approach for mixed-signal verification. In Proceedings of the 14th Workshop on Synthesis and System Integration of Mixed Information Technologies. 507--514."},{"volume-title":"Proceedings of the Asian Symposium on Programming Languages and Systems. 322--338","author":"Li G.","key":"e_1_2_1_13_1","unstructured":"Li , G. and Tang , Z . 2003. Translating a continuous-time temporal logic into timed automata . In Proceedings of the Asian Symposium on Programming Languages and Systems. 322--338 . Li, G. and Tang, Z. 2003. Translating a continuous-time temporal logic into timed automata. In Proceedings of the Asian Symposium on Programming Languages and Systems. 322--338."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science","volume":"3253","author":"Maler O.","unstructured":"Maler , O. and Nickovic , D . 2004. Monitoring temporal properties of continuous signals . In Proceedings of the International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science , vol. 3253 . Springer, 152--166. Maler, O. and Nickovic, D. 2004. Monitoring temporal properties of continuous signals. In Proceedings of the International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science, vol. 3253. Springer, 152--166."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11603009_2"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Maler O. Nickovic D. and Pnueli A. 2008. Checking temporal properties of discrete timed and continuous behaviors. In Pillars of Computer Science 475--505. Maler O. Nickovic D. and Pnueli A. 2008. Checking temporal properties of discrete timed and continuous behaviors. In Pillars of Computer Science 475--505.","DOI":"10.1007\/978-3-540-78127-1_26"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.01.019"},{"key":"e_1_2_1_18_1","unstructured":"Mukherjee S. and Dasgupta P. 2011. AMS-LTL properties: Samples from industrial test cases. http:\/\/www.facweb.iithgp.ernet.in\/~pallab\/PMU.pdf. Mukherjee S. and Dasgupta P. 2011. AMS-LTL properties: Samples from industrial test cases. http:\/\/www.facweb.iithgp.ernet.in\/~pallab\/PMU.pdf."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2011.2155065"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1497561.1497564"},{"volume-title":"Proceedings of the International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). 304--319","author":"Nickovic D.","key":"e_1_2_1_22_1","unstructured":"Nickovic , D. and Maler , O . 2007. Amt: A property-based monitoring tool for analog systems . In Proceedings of the International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). 304--319 . Nickovic, D. and Maler, O. 2007. Amt: A property-based monitoring tool for analog systems. In Proceedings of the International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). 304--319."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1403375.1403453"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Sundararajan D. 2003. Digital Signal Processing: Theory and Practice. World Scientific. Sundararajan D. 2003. Digital Signal Processing: Theory and Practice . World Scientific.","DOI":"10.1142\/5147"},{"key":"e_1_2_1_26_1","unstructured":"Verilog-AMS. 2010. Verilog-AMS language reference manual. www.eda.org\/verilog-ams\/. Verilog-AMS . 2010. Verilog-AMS language reference manual. www.eda.org\/verilog-ams\/."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/65294.71210"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11856290_20"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2348839.2348842","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2348839.2348842","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:02Z","timestamp":1750278122000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2348839.2348842"}},"subtitle":["From Theory to Practice"],"short-title":[],"issued":{"date-parts":[[2012,10]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,10]]}},"alternative-id":["10.1145\/2348839.2348842"],"URL":"https:\/\/doi.org\/10.1145\/2348839.2348842","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2012,10]]},"assertion":[{"value":"2010-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}