{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T06:53:26Z","timestamp":1672383206469},"reference-count":37,"publisher":"Elsevier BV","issue":"4-5","license":[{"start":{"date-parts":[[2005,6,1]],"date-time":"2005-06-01T00:00:00Z","timestamp":1117584000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computers & Electrical Engineering"],"published-print":{"date-parts":[[2005,6]]},"DOI":"10.1016\/j.compeleceng.2005.04.001","type":"journal-article","created":{"date-parts":[[2005,7,28]],"date-time":"2005-07-28T21:24:29Z","timestamp":1122585869000},"page":"282-302","source":"Crossref","is-referenced-by-count":9,"title":["An automatic ABV methodology enabling PSL assertions across SLD flow for SOCs modeled in SystemC"],"prefix":"10.1016","volume":"31","author":[{"given":"Younes","family":"Lahbib","sequence":"first","affiliation":[]},{"given":"Romain","family":"Kamdem","sequence":"additional","affiliation":[]},{"given":"Mohamed-lyes","family":"Benalycherif","sequence":"additional","affiliation":[]},{"given":"Rached","family":"Tourki","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.compeleceng.2005.04.001_bib1","unstructured":"Ali H, Sofiene T. On the extension of SystemVerilog assertion. In: CCECE\/CCGEI, IEEE, Niagara Falls, May 2004."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib2","unstructured":"SystemC Homepage, 2004. Available from: ."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib3","series-title":"Assertion-based design","author":"Foster","year":"2003"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib4","series-title":"System design with SystemC","author":"Thorsten","year":"2003"},{"issue":"8","key":"10.1016\/j.compeleceng.2005.04.001_bib5","article-title":"Logic of constraints: a quantitative performance and functional constraint formalism","volume":"23","author":"Chen","year":"2004","journal-title":"IEEE Trans Comput-Aid Des Integrated Circ Syst"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib6","unstructured":"Marshner E, Deadman B, Martin G. IP reuse hardening via embedded sugar assertion. In: IP based SOC design, October 30\u201331, 2002."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib7","unstructured":"Bassam T, George B, Dave K. Challenges and opportunities for debug at the system level: debugging SystemC models. In: SAME04, San Jose, USA, October 6\u20137, 2004."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib8","unstructured":"PSL Homepage, 2003. Available from: ."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib9","unstructured":"System Verilog Assertions Homepage, 2003. Available from: ."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib10","unstructured":"OpenVera Assertions White Paper. Synopsys, Inc. Mountain View, CA, 2002."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib11","doi-asserted-by":"crossref","unstructured":"Abranel Y, Beer I, Glushovsky L, Keider S, Wolfsthal Y. FoCs-automatic generation of simulation checkers from formal specifications. In: Proc. computer-aided conference (CAV), 2000. p. 538\u201342.","DOI":"10.1007\/10722167_40"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib12","unstructured":"Users Manual FoCs, Formal checkers\u2014a productivity tool version 1.05 with Sugar2 support (EDL avor), Formal Methods and Technologies Group. IBM Research Lab in Haifa, January 2004."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib13","doi-asserted-by":"crossref","unstructured":"Dahan A, Geist D, Gluhovsky L, Pidan D, Shapir G, Wolfsthal Y. Combining system level modeling with assertion based verification. In: The sixth international symposium on quality of electronic design (ISQED\u201905), IEEE, San Jose, CA, March 21\u201323, 2005.","DOI":"10.1109\/ISQED.2005.32"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib14","unstructured":"Open Verification Library, Inc. Homepage, 2005. Available from: ."},{"issue":"December","key":"10.1016\/j.compeleceng.2005.04.001_bib15","doi-asserted-by":"crossref","first-page":"1523","DOI":"10.1109\/43.898830","article-title":"System level design: orthogonalization of concerns and platform-based design","volume":"19","author":"Keutzer","year":"2000","journal-title":"IEEE Trans Comput-Aid Des"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib16","series-title":"Proc, 13th conference on computer aided verification (CAV01)","first-page":"68","article-title":"A practical approach to coverage in model checking","volume":"vol. 2102","author":"Chockler","year":"2001"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib17","doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Eisner C, Landver A. RuleBase: an industry-oriented formal verification tool. In: Proc on design automation conference DAC\u201996, Las Vegas, NV, June 1996. p. 655\u201360.","DOI":"10.1145\/240518.240642"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib18","unstructured":"Goering Richard. 0-In revs assertion-based verification. In: EEDesign, April 19, 2002."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib19","series-title":"Proc design automation and test in Europe (DATE\u201999)","first-page":"145","article-title":"Combinational equivalence checking using satisfiability and recursive learning","author":"Marques-Silva","year":"1999"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib20","doi-asserted-by":"crossref","unstructured":"Shimizu K, Dill DL. Derivinga simulation input generator and a coverage metric from a formal specification. In: IEEE\/ACM design automation conference, 2002. p. 801\u20136.","DOI":"10.1145\/513918.514118"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib21","unstructured":"Cadence Design Systems, Inc. Simulation-based assertion checking user guide. Product Version 5.3, April 2004."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib22","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/S0045-7906(04)00019-9","article-title":"Co-simulation and communication synthesis approach for intellectual properties based SoCs","author":"Marzougui","year":"2004","journal-title":"Comput Electr Eng"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib23","doi-asserted-by":"crossref","unstructured":"Dill D. What\u2019s between simulation and formal verification? In: Invited lecture in design automation conference DAC\u201998, San Francisco, CA, USA, June 1998.","DOI":"10.1109\/DAC.1998.724491"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib24","doi-asserted-by":"crossref","unstructured":"Pnueli A. The temporal logic of programs. In: Proc. 18th IEEE sympos. foundation comput. sci., 1977. p. 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib25","unstructured":"Ho Richard. Counter-examples and metrics drive assertion-based verification. In: EEDesign, January 2003."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib26","series-title":"Symbolic model checking","author":"McMillan","year":"1993"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib27","unstructured":"Caldari M, Conti M, Coppola M, Curaba S, Pieralisi L, Turchetti C. Transaction-level models for AMBA bus architecture using SystemC 2.0, 2003."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib28","unstructured":"Ogawa O et al. A practical approach for bus architecture optimization at transaction level, 2003."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib29","doi-asserted-by":"crossref","unstructured":"Pasricha S, Dutt N, Ben-Romdhane M. Extending the transaction level modeling approach for fast communication architecture exploration. In: DAC.04, June 7\u201311, 2004, San Diego, CA, USA.","DOI":"10.1145\/996566.996603"},{"issue":"May","key":"10.1016\/j.compeleceng.2005.04.001_bib30","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker SPIN","volume":"23","author":"Holzmann","year":"1997","journal-title":"IEEE Trans Software Eng"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib31","doi-asserted-by":"crossref","unstructured":"Ruf J, Hoffmann DW, Kropf T, Rosenstiel W. Simulation-guided property checking based on multi-valued AR-automata. In: IEEE design automation and test in Europe, 2001. p. 742\u20138.","DOI":"10.1109\/DATE.2001.915111"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib32","series-title":"Writing test benches. Functional verification of HDL models","author":"Bergeron","year":"2003"},{"key":"10.1016\/j.compeleceng.2005.04.001_bib33","unstructured":"William S, David G, Neil R, James G. Using VTOC for large SoC concurrent engineering: a real world case study. In: DesignCon 2003 system-on-chip and ASIC conference."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib34","unstructured":"Ho P-H et al. Smart simulation using collaborative formal and simulation engine. In: IEEE\/ACM international conference on CAD, 2000. p. 120\u20136."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib35","unstructured":"Prosilog, Inc. Homepage, 2004. Available from: ."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib36","unstructured":"Carbon Design Systems, Inc. Homepage, 2004. Available from: ."},{"key":"10.1016\/j.compeleceng.2005.04.001_bib37","series-title":"Proc. 11th Int. (CAV\u201999)","article-title":"Verifying safety properties of a power PC (tm) microprocessor using symbolic model checking without BDDs","author":"Biere","year":"1999"}],"container-title":["Computers & Electrical Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0045790605000613?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0045790605000613?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T11:50:05Z","timestamp":1586346605000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0045790605000613"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,6]]},"references-count":37,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2005,6]]}},"alternative-id":["S0045790605000613"],"URL":"http:\/\/dx.doi.org\/10.1016\/j.compeleceng.2005.04.001","relation":{},"ISSN":["0045-7906"],"issn-type":[{"value":"0045-7906","type":"print"}],"subject":["Electrical and Electronic Engineering","General Computer Science","Control and Systems Engineering"],"published":{"date-parts":[[2005,6]]}}}