{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T10:24:57Z","timestamp":1725618297570},"publisher-location":"New York, NY, USA","reference-count":12,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2005,4,17]]},"DOI":"10.1145\/1057661.1057756","type":"proceedings-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T04:31:47Z","timestamp":1123043507000},"page":"400-403","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Exploiting PSL standard assertions in a theorem-proving-based verification environment"],"prefix":"10.1145","author":[{"given":"Youngsik","family":"Kim","sequence":"first","affiliation":[{"name":"Syracuse University, Syracuse, New York"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Parija","family":"Sule","sequence":"additional","affiliation":[{"name":"Syracuse University, Syracuse, New York"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nazanin","family":"Mansouri","sequence":"additional","affiliation":[{"name":"Syracuse University, Syracuse, New York"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,4,17]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Accellera. Accellera Standard SystemVerilog 3.1 April 2003.  Accellera. Accellera Standard SystemVerilog 3.1 April 2003."},{"volume-title":"Assertion Monitor Reference Manual","year":"2003","author":"Accellera Organization","key":"e_1_3_2_1_2_1"},{"key":"e_1_3_2_1_3_1","unstructured":"Accellera Organization. Property Specification Language Reference Manual 2004.  Accellera Organization. Property Specification Language Reference Manual 2004."},{"key":"e_1_3_2_1_4_1","unstructured":"S. Berezin. The SYMP tool. WWW URL: http:\/\/www.cms.edu\/modelcheck\/symp.html 2001.  S. Berezin. The SYMP tool. WWW URL: http:\/\/www.cms.edu\/modelcheck\/symp.html 2001."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/861854"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"M. Gordon J. Hurd and K. Slind. Executing the formal semantics of the accellera property specification language by mechanised theorem proving. 2003.  M. Gordon J. Hurd and K. Slind. Executing the formal semantics of the accellera property specification language by mechanised theorem proving. 2003.","DOI":"10.1007\/978-3-540-39724-3_19"},{"key":"e_1_3_2_1_7_1","unstructured":"R. Ho. Assertions aid design for verification strategy.  R. Ho. Assertions aid design for verification strategy."},{"key":"e_1_3_2_1_8_1","unstructured":"D. Korening. Application specification higher order logic theorem proving. 2002.  D. Korening. Application specification higher order logic theorem proving. 2002."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"T. Kropf. Benchmark-Circuits for Hardware-Verification 1994. www:http:\/\/goethe.ira.uka.de\/hvg\/.  T. Kropf. Benchmark-Circuits for Hardware-Verification 1994. www:http:\/\/goethe.ira.uka.de\/hvg\/.","DOI":"10.1007\/3-540-59047-1_39"},{"key":"e_1_3_2_1_10_1","unstructured":"C.-J. H. S. Mark D. Aagaard. The formal verification of a pipelined double-precision ieee floating-point multiplier. 1995.   C.-J. H. S. Mark D. Aagaard. The formal verification of a pipelined double-precision ieee floating-point multiplier. 1995."},{"volume-title":"SRI International","year":"2001","author":"Owre S.","key":"e_1_3_2_1_11_1"},{"key":"e_1_3_2_1_12_1","unstructured":"A. G. R. Boulton M. Gordon J. Harrison J. Herbert and J. Tassel. Experience with embedding hardware description language in hol. 1992.   A. G. R. Boulton M. Gordon J. Harrison J. Herbert and J. Tassel. Experience with embedding hardware description language in hol. 1992."}],"event":{"name":"GLSVLSI05: Great Lakes Symposium on VLSI 2005","sponsor":["ACM Association for Computing Machinery","SIGDA ACM Special Interest Group on Design Automation"],"location":"Chicago Illinois USA","acronym":"GLSVLSI05"},"container-title":["Proceedings of the 15th ACM Great Lakes symposium on VLSI"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1057661.1057756","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T11:41:55Z","timestamp":1673437315000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1057661.1057756"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,4,17]]},"references-count":12,"alternative-id":["10.1145\/1057661.1057756","10.1145\/1057661"],"URL":"https:\/\/doi.org\/10.1145\/1057661.1057756","relation":{},"subject":[],"published":{"date-parts":[[2005,4,17]]},"assertion":[{"value":"2005-04-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}