{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T05:25:26Z","timestamp":1739424326791,"version":"3.37.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2009,10,13]],"date-time":"2009-10-13T00:00:00Z","timestamp":1255392000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Electron Test"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1007\/s10836-009-5116-4","type":"journal-article","created":{"date-parts":[[2009,10,12]],"date-time":"2009-10-12T10:13:30Z","timestamp":1255342410000},"page":"289-300","source":"Crossref","is-referenced-by-count":5,"title":["PSL Assertion Checking Using Temporally Extended High-Level Decision Diagrams"],"prefix":"10.1007","volume":"25","author":[{"given":"Maksim","family":"Jenihhin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jaan","family":"Raik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton","family":"Chepurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raimund","family":"Ubar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,10,13]]},"reference":[{"key":"5116_CR1","unstructured":"Accellera, Property specification language reference manual, v1.1, June 9, 2004"},{"key":"5116_CR2","doi-asserted-by":"crossref","unstructured":"Boul\u00e9 M, Zilic Z (2006) Efficient automata-based assertion-checker synthesis of PSL properties. Proceedings of the IEEE International High Level Design Validation and Test Workshop (HLDVT\u201906)","DOI":"10.1109\/HLDVT.2006.319966"},{"issue":"8","key":"5116_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R Bryant","year":"1986","unstructured":"Bryant R (1986) Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35(8):677\u2013691","journal-title":"IEEE Transactions on Computers"},{"key":"5116_CR4","unstructured":"Bustan D, Fisman D, Havlicek J. Automata construction for PSL. The Weizmann Institute of Science, Technical Report MCS05-04"},{"key":"5116_CR5","doi-asserted-by":"crossref","unstructured":"Chayakul V, Gajski DD, Ramachandran L (1993) High-level transformations for minimizing syntactic variances. Proc. of the ACM\/IEEE Design Automation Conference (DAC), pp. 413\u2013418, June 1993","DOI":"10.1145\/157485.164956"},{"key":"5116_CR6","unstructured":"Clarke E, Fujita M, McGeer P, McMillan KL, Yang J, Zhao X (1993) Multi terminal BDDs: an efficient data structure for matrix representation. Proc. of the International Workshop on Logic Synthesis, pp. P6a:1\u201315"},{"key":"5116_CR7","doi-asserted-by":"crossref","unstructured":"Drechsler R, Becker B, Ruppertz S (1996) K*BMDs: a new data structure for verification. Proc. of the European Design & Test Conference, pp. 2\u20138","DOI":"10.1109\/EDTC.1996.494118"},{"key":"5116_CR8","unstructured":"Eisner C, Fisman D (2006) A practical introduction to PSL. Springer Science"},{"key":"5116_CR9","unstructured":"Gheorghita S, Grigore R (2005) Constructing checkers from PSL properties. 15th International Conference on Control Systems and Computer Science (CSCS15), 2:757\u2013762"},{"key":"5116_CR10","unstructured":"IBM AlphaWorks (2007) FoCs Property Checkers Generator ver. 2.04, [ www.alphaworks.ibm.com\/tech\/FoCs ]"},{"key":"5116_CR11","unstructured":"IEEE-Commission, IEEE standard for Property Specification Language (PSL), (2005) IEEE Std 1850\u20132005"},{"key":"5116_CR12","unstructured":"ITC99 Benchmark Home Page. URL: http:\/\/www.cerc.utexas.edu\/itc99-benchmarks\/bench.html"},{"key":"5116_CR13","unstructured":"ITRS Roadmap. URL: http:\/\/www.itrs.net"},{"key":"5116_CR14","unstructured":"Jenihhin M, Raik J, Chepurov A, Ubar R (2007) Assertion checking with PSL and high-level decision diagrams. IEEE Workshop on RTL and High Level Testing (WRTLT\u201907), October 12\u201313, 2007"},{"key":"5116_CR15","doi-asserted-by":"crossref","unstructured":"Morin-Allory K, Borrione D (2006) Proven correct monitors from PSL specifications, Proceedings of the IEEE\/ACM Design, Automation & Test in Europe (DATE)","DOI":"10.1109\/DATE.2006.244079"},{"key":"5116_CR16","doi-asserted-by":"crossref","unstructured":"Oddos Y, Morin-Allory K, Borrione D (2007) Prototyping generators for on-line test vector generation based on PSL properties. Proceedings of the 10th IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS 2007), pp 383\u2013388","DOI":"10.1109\/DDECS.2007.4295317"},{"key":"5116_CR17","unstructured":"Raik J, Ubar R (2000) Fast test generation for sequential circuits using decision diagrams representations. Journal of Electronic Testing: Theory and Applications, Kluwer"},{"issue":"1","key":"5116_CR18","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/s10836-005-5288-5","volume":"21","author":"J Raik","year":"2005","unstructured":"Raik J, N\u00f5mmeots T, Ubar R (2005) A new testability calculation method to guide RTL test generation. Journal of Electronic Testing: Theory and Applications 21(1):71\u201382 Springer Science","journal-title":"Journal of Electronic Testing: Theory and Applications"},{"key":"5116_CR19","doi-asserted-by":"crossref","unstructured":"Raik J, Fujiwara H, Ubar R, Krivenko A (2008) Untestable fault identification in sequential circuits using model-checking, IEEE Asian Test Symposium","DOI":"10.1109\/ATS.2008.22"},{"issue":"3\u20134","key":"5116_CR20","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1016\/j.sysarc.2007.07.003","volume":"54","author":"J Raik","year":"2008","unstructured":"Raik J, Ubar R, Viilukas T, Jenihhin M (2008) Mixed hierarchical-functional fault models for targeting sequential cores. Elsevier Journal of Systems Architecture 54(3\u20134):465\u2013477 Elsevier","journal-title":"Elsevier Journal of Systems Architecture"},{"key":"5116_CR21","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1109\/ISCAS.2000.857064","volume":"1","author":"R Ubar","year":"2000","unstructured":"Ubar R, Raik J, Morawiec A (2000) Back-tracing and event-driven techniques in high-level simulation with decision diagrams. The IEEE International Symposium on Circuits and Systems (ISCAS 2000) 1:208\u2013211","journal-title":"The IEEE International Symposium on Circuits and Systems (ISCAS 2000)"},{"key":"5116_CR22","doi-asserted-by":"crossref","unstructured":"Ubar R (1996) Test synthesis with alternative graphs. In IEEE Design and Test of Computers, pp 48\u201357","DOI":"10.1109\/54.485782"},{"key":"5116_CR23","unstructured":"Yuan J, Pixley C, Aziz A (2006) Constraint-based verification. Springer"}],"container-title":["Journal of Electronic Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-009-5116-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10836-009-5116-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-009-5116-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T18:12:17Z","timestamp":1739383937000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10836-009-5116-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,10,13]]},"references-count":23,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["5116"],"URL":"https:\/\/doi.org\/10.1007\/s10836-009-5116-4","relation":{},"ISSN":["0923-8174","1573-0727"],"issn-type":[{"type":"print","value":"0923-8174"},{"type":"electronic","value":"1573-0727"}],"subject":[],"published":{"date-parts":[[2009,10,13]]}}}