{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:33:34Z","timestamp":1750307614299,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2009,3,1]],"date-time":"2009-03-01T00:00:00Z","timestamp":1235865600000},"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":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2009,3]]},"abstract":"<jats:p>\n            The industry trend appears to be moving towards designs that integrate large digital circuits with multiple analog\/RF (radio frequency) interfaces. In the verification of these large integrated circuits, the number of nets that need to be monitored has been growing rapidly. Consequently, the mixed-signal design community has been feeling the need for AMS (Analog and Mixed Signal) assertions that can automatically monitor conformance with expected time-domain behavior and help in debugging deviations from the design intent. The main challenges in providing this support are (a) developing AMS assertion languages or AMS verification libraries, and (b) instrumenting existing commercial simulators to support assertion verification during simulation. In this article, we report two approaches: the first extends the\n            <jats:italic>Open Verification Library<\/jats:italic>\n            (OVL) to the AMS domain by integrating a new collection of AMS verification libraries; while the second extends\n            <jats:italic>SystemVerilog Assertions<\/jats:italic>\n            (SVA) by augmenting analog predicates into SVA. We demonstrate the use of AMS-OVL on the Cadence Virtuoso environment while emphasizing that our libraries can work in any environment that supports Verilog and Verilog-A. We also report the development of tool support for AMS-SVA using a combination of Cadence NCSIM and Synopsys VCS. We demonstrate the utility of both approaches on the verification of LP3918, an integrated power management unit (PMU) from National Semiconductors. We believe that in the absence of existing EDA (Electronic Design Automation) tools for AMS assertion verification, the proposed approaches of integrating our libraries and our tool sets with existing commercial simulators will be of considerable and immediate practical value.\n          <\/jats:p>","DOI":"10.1145\/1497561.1497564","type":"journal-article","created":{"date-parts":[[2009,4,6]],"date-time":"2009-04-06T16:34:22Z","timestamp":1239035662000},"page":"1-47","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Instrumenting AMS assertion verification on commercial platforms"],"prefix":"10.1145","volume":"14","author":[{"given":"Rajdeep","family":"Mukhopadhyay","sequence":"first","affiliation":[{"name":"IIT Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S. K.","family":"Panda","sequence":"additional","affiliation":[{"name":"IIT Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pallab","family":"Dasgupta","sequence":"additional","affiliation":[{"name":"IIT Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Gough","sequence":"additional","affiliation":[{"name":"National Semiconductor Corp., Greenock, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,4,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_2_1_3_1","unstructured":"AMS-User-Guide. Virtuoso AMS Environment User Guide. www.ece.osu.edu\/~bibyk\/ee894z\/\\\\amsenvug.pdf.  AMS-User-Guide. Virtuoso AMS Environment User Guide. www.ece.osu.edu\/~bibyk\/ee894z\/\\\\amsenvug.pdf."},{"volume-title":"Proceedings of the IEEE VLSI Test Symposium. 42--47","author":"Balivada A.","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/BMAS.2004.1393990"},{"volume-title":"Proceedings of the Formal Methods In Computer-aided Design:5th International Conference (FMCAD).","author":"Dang T.","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICVD.2005.38"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_17"},{"volume-title":"Proceedings of the Conference on Design, Automation and Test in Europe. 257--262","author":"Frehse G.","key":"e_1_2_1_10_1"},{"volume-title":"Proceedings of the International Conference on Computer Design. 40--45","author":"Ghosh A.","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382573"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/646521.759250"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008791128550"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Hartong W. Klausen R. and Hedrich L. 2004. Formal verification for nonlinear analog systems. In Approaches to Model and Equivalence Checking. Advanced Formal Verification Kluwer Amsterdam 205--245.  Hartong W. Klausen R. and Hedrich L. 2004. Formal verification for nonlinear analog systems. In Approaches to Model and Equivalence Checking. Advanced Formal Verification Kluwer Amsterdam 205--245.","DOI":"10.1007\/1-4020-2530-0_6"},{"volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design. 123--127","author":"Hedrich L.","key":"e_1_2_1_16_1"},{"volume-title":"Proceedings of the Conference on Design, Automation and Test in Europe.","author":"Hedrich L.","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"volume-title":"Proceedings of the Conference on Asia and South Pacific Design Automation. IEEE Computer Society Press","author":"Jesser A.","key":"e_1_2_1_19_1"},{"volume-title":"Proceedings of the Workshop on Synthesis and System Integrating of Mixed Information Technologies (SASIMI). 507--514","author":"Jesser A.","key":"e_1_2_1_20_1"},{"volume-title":"The Designer's Guide to Verilog-AMS","author":"Kundert K.","key":"e_1_2_1_21_1"},{"key":"e_1_2_1_22_1","unstructured":"LP3918. http:\/\/www.national.com\/pf\/LP\/LP3918.html.  LP3918. http:\/\/www.national.com\/pf\/LP\/LP3918.html."},{"key":"e_1_2_1_23_1","first-page":"1","article-title":"Extending PSL for analog circuits. Res. rep","volume":"1","author":"Maler O.","year":"2005","journal-title":"PROSYD Deliverable D"},{"volume":"3253","volume-title":"Proceedings of the Conference Formal Techniques, Modeling and Analysis of Timed and Fault-Tolerant Systems. Lecture Notes in Computer Science","author":"Maler O.","key":"e_1_2_1_24_1"},{"key":"e_1_2_1_25_1","unstructured":"Maler O. Pnueli A. and Nickovic D. 2008. Checking temporal properties of discrete timed and continuous behaviors. Trakhtenbrot Festschrift.  Maler O. Pnueli A. and Nickovic D. 2008. Checking temporal properties of discrete timed and continuous behaviors. Trakhtenbrot Festschrift."},{"key":"e_1_2_1_26_1","unstructured":"MLD. MLDesigner documentation version 2.5. http:\/\/www.mldesigner.com.  MLD. MLDesigner documentation version 2.5. http:\/\/www.mldesigner.com."},{"volume-title":"Proceedings of the 5th International Conference on Formats.","author":"Nickovic D.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","unstructured":"OVL. Open Verification Library. http:\/\/www.accellera.org\/activities\/ovl.  OVL. Open Verification Library. http:\/\/www.accellera.org\/activities\/ovl."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/BMAS.2006.283462"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2002.1010708"},{"volume-title":"Proceedings of the Conference on Languages for Formal Specification and Verification (FDL).","year":"2007","author":"Sammane G. A.","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","unstructured":"SVA. System Verilog Assertions. http:\/\/www.systemverilog.org.  SVA. System Verilog Assertions. http:\/\/www.systemverilog.org."},{"key":"e_1_2_1_33_1","unstructured":"Verilog AMS LRM. www.verilog.org\/verilogams\/htmlpages\/publicdocs\/lrm\/2.2\/AMS-LRM-2-2.pdf.  Verilog AMS LRM. www.verilog.org\/verilogams\/htmlpages\/publicdocs\/lrm\/2.2\/AMS-LRM-2-2.pdf."},{"key":"e_1_2_1_34_1","unstructured":"Verilog-XL-Env-User-Guide. Virtuoso Verilog-XL Environment User Guide Product Version 5.1.41. http:\/\/www.ece.uci.edu\/eceware\/cadence\/compveruser\/chap9.html.  Verilog-XL-Env-User-Guide. Virtuoso Verilog-XL Environment User Guide Product Version 5.1.41. http:\/\/www.ece.uci.edu\/eceware\/cadence\/compveruser\/chap9.html."},{"volume-title":"Proceedings of the Conference on Automated Technology for Verification and Analysis","series-title":"Lecture Notes in Computer Science","author":"Walter D.","key":"e_1_2_1_35_1"},{"volume-title":"Proceedings of the IEEE Northeast Workshop on Circuits and Systems. 281--284","author":"Zaki M.","key":"e_1_2_1_36_1"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1497561.1497564","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1497561.1497564","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:45:43Z","timestamp":1750250743000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1497561.1497564"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,3]]}},"alternative-id":["10.1145\/1497561.1497564"],"URL":"https:\/\/doi.org\/10.1145\/1497561.1497564","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2009,3]]},"assertion":[{"value":"2008-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-04-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}