{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T19:35:15Z","timestamp":1743017715932,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":42,"publisher":"Springer Singapore","isbn-type":[{"type":"print","value":"9789813297661"},{"type":"electronic","value":"9789813297678"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-981-32-9767-8_41","type":"book-chapter","created":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T02:02:54Z","timestamp":1566007374000},"page":"496-509","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Functional Simulation Verification of RISC-V Instruction Set Based High Level Language Modeled FPU"],"prefix":"10.1007","author":[{"given":"Aneesh","family":"Raveendran","sequence":"first","affiliation":[]},{"given":"Vinay","family":"Kumar","sequence":"additional","affiliation":[]},{"given":"D.","family":"Vivian","sequence":"additional","affiliation":[]},{"given":"David","family":"Selvakumar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,18]]},"reference":[{"key":"41_CR1","doi-asserted-by":"crossref","unstructured":"Goni, O., Todorovich, E., et al.: Generic construction of monitors for floating point unit designs. In: 2012 VIII Southern Conference on Programmable Logic (2012)","DOI":"10.1109\/SPL.2012.6211776"},{"key":"41_CR2","unstructured":"Hauser, J.: \u201cSoftfloat\u201d technical Report - International Computer Science Institute (2010). \n                    http:\/\/www.jhauser.us\/arithmetic\/SoftFloat.html"},{"key":"41_CR3","unstructured":"Cowlishaw, M.: The decNumber C library, 3rd ed. IBM Corp. (2008). \n                    https:\/\/www.ibm.com\/support\/knowledgecenter\/en\/SSB23S_1.1.0.15\/gtpa2\/pkdecsp.html\n                    \n                  , \n                    http:\/\/mirrors.josefsipek.net\/speleotrove.com\/decimal\/decnumber.pdf"},{"key":"41_CR4","unstructured":"Brunelli, C., Nurmi, J., et al.: Design and verification of a VHDL model of a floating-point unit for a RISC microprocessor. In: IEEE International Symposium on System-on-Chip (2016)"},{"key":"41_CR5","doi-asserted-by":"crossref","unstructured":"Chen, C.I., Yu, C.Y., Lu, Y.J., Wu, C.F.: Apply high-level synthesis design and verification methodology on floating-point unit implementation. In: International Symposium on VLSI Design, Automation and Test (VLSI-DAT) (2014)","DOI":"10.1109\/VLSI-DAT.2014.6834921"},{"key":"41_CR6","unstructured":"EEMBC FPMark. \n                    https:\/\/www.eembc.org\/fpmark\/"},{"key":"41_CR7","doi-asserted-by":"crossref","unstructured":"Pachiana, G., Rodriguez, J.A.: Coverage modeling for verification of floating point Arithmetic units. In: Argentine School of Micro-Nanoelectronics, Technology and Applications (2014)","DOI":"10.1109\/EAMTA.2014.6906084"},{"key":"41_CR8","unstructured":"IBM Floating Point Test Generator. \n                    https:\/\/www.research.ibm.com\/haifa\/projects\/verification\/fpgen\/"},{"key":"41_CR9","doi-asserted-by":"crossref","unstructured":"Go\u00f1i, O., Todorovich, E., et al.: Components for coverage-driven verification of floating-point units. In: IEEE IX Southern Conference on Programmable Logic (SPL) (2014)","DOI":"10.1109\/SPL.2014.7002208"},{"key":"41_CR10","doi-asserted-by":"crossref","unstructured":"Krautz, U., Paruthi, V., et al.: Automatic verification of floating point units. In: Proceedings of 51st Annual Design Automation, DAC 2014 (2014)","DOI":"10.1145\/2593069.2593096"},{"key":"41_CR11","doi-asserted-by":"crossref","unstructured":"Guralnik, E., Birnbaum, A.J., Koyfman, A., et al.: Implementation specific verification of divide and square root instructions. In: 19th IEEE International Symposium on Computer Arithmetic (2009)","DOI":"10.1109\/ARITH.2009.24"},{"key":"41_CR12","unstructured":"Duale, A.Y., Decker, M.H., et al.: Decimal floating-point in z9: an implementation and testing perspective. \n                    http:\/\/research.ibm.com\/haifa\/projects\/verification\/fpgen\/papers\/duale.pdf"},{"key":"41_CR13","unstructured":"Jacobi, C., et al.: Automatic formal verification of fused-multiply-add FPUs. \n                    https:\/\/www.research.ibm.com\/haifa\/projects\/verification\/SixthSense\/papers\/flavor_date_05.pdf"},{"key":"41_CR14","unstructured":"Aharoni, M., et al.: FPgen \u2013 a test generation framework for datapath floating-point verification. In: Eighth IEEE International High-Level Design Validation and Test Workshop (2003)"},{"issue":"2","key":"41_CR15","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1109\/TC.2010.165","volume":"60","author":"Elena Guralnik","year":"2011","unstructured":"Guralnik, E., et al.: Simulation-Based Verification of Floating-Point Division (2011). \n                    https:\/\/www.research.ibm.com\/haifa\/projects\/verification\/fpgen\/papers\/Simulation_Based_Verification_of_Floating_Point_Division.pdf","journal-title":"IEEE Transactions on Computers"},{"key":"41_CR16","unstructured":"Seidel, P.-M.: Formal verification of an iterative low-power x86floating-pointmultiplier with redundant feedback. \n                    https:\/\/arxiv.org\/pdf\/1110.4675.pdf"},{"key":"41_CR17","unstructured":"Kiran Kumar, M.A., et al.: Symbolic trajectory evaluation: the primary validation vehicle for next generation intel\u00ae processor graphics FPU. \n                    http:\/\/www.cs.utexas.edu\/~hunt\/fmcad\/FMCAD12\/025.pdf"},{"key":"41_CR18","unstructured":"Ouchani, S., et al.: A formal verification framework for bluespec system verilog in specification & design languages (FDL) (2013)"},{"key":"41_CR19","unstructured":"OMG: OMG Systems Modelling Language (OMG SysML) Specification, Object Management Group. \n                    http:\/\/www.omgsysml.org\/"},{"key":"41_CR20","unstructured":"Bluespec inc. \n                    http:\/\/www.bluespec.com"},{"key":"41_CR21","unstructured":"Singh, G., et al.: Model-checking based verification for hardware designs specified using bluespec system verilog. In: IEEE 8th International Workshop on Test and Verification (2007)"},{"key":"41_CR22","unstructured":"Beyer, S.: The application of formal technology on fixed-point arithmetic systemC designs. In: Design and Verification Conference and Exhibition. One spin soluution (2015)"},{"key":"41_CR23","unstructured":"Ram, R.: Formal verification of floating point hardware with assertion based VIP. In: Design and Verification Conference and Exhibition. One spin solutions (2018)"},{"key":"41_CR24","unstructured":"Travis, W., Pouarz, V., et al.: Efficient and exhaustive floating point verification using sequential equivalence checking. In: DVCon (2017)"},{"key":"41_CR25","doi-asserted-by":"publisher","first-page":"774","DOI":"10.1109\/TCAD.2012.2232351","volume":"32","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., et al.: Software model checking SystemC. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 32, 774\u2013787 (2013)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"41_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-22110-1_24","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2011","unstructured":"Cimatti, A., Griggio, A., Micheli, A., Narasamdya, I., Roveri, M.: Kratos \u2013 a software model checker for SystemC. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 310\u2013316. Springer, Heidelberg (2011). \n                    https:\/\/doi.org\/10.1007\/978-3-642-22110-1_24"},{"key":"41_CR27","unstructured":"Herber, P., et al.: Formal verification of SystemC designs using the BLAST software model checker. In: International Workshop on Model-Based Architecting and Construction of Embedded Systems (ACES-MB) (2013)"},{"key":"41_CR28","doi-asserted-by":"crossref","unstructured":"Ngo, V.C., et al.: Statistical model checking for SystemC models. In: IEEE 17th International Symposium on High Assurance Systems Engineering (HASE) (2016)","DOI":"10.1109\/HASE.2016.24"},{"key":"41_CR29","unstructured":"Oscar, O.: On the Formal Semantics of Bluespec System Verilog, Thesis (2013)"},{"key":"41_CR30","unstructured":"Hauksson, H.: Towards model checking BSV in Uppaal, MscThesis (2013)"},{"key":"41_CR31","unstructured":"Singh, G., et al.: Model checking bluespec specified hardware designs. In: Eighth International Workshop on Microprocessor Test and Verification (2017)"},{"key":"41_CR32","unstructured":"Richards, D., et al.: A prototype embedding of bluespec system verilog in the PVS theorem prover. In: Second NASA Formal Methods Symposium, NFM 2010 (2010)"},{"key":"41_CR33","unstructured":"Richards, D., et al.: A prototype embedding of bluespec systemverilog in the SAL model checker. \n                    http:\/\/www.cs.ox.ac.uk\/dcc2010\/slides\/richards.pdf"},{"key":"41_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-540-85114-1_18","volume-title":"Model Checking Software","author":"G Singh","year":"2008","unstructured":"Singh, G., Shukla, Sandeep K.: Verifying compiler based refinement of bluespecTM specifications using the SPIN model checker. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 250\u2013269. Springer, Heidelberg (2008). \n                    https:\/\/doi.org\/10.1007\/978-3-540-85114-1_18"},{"key":"41_CR35","unstructured":"Raveendran, A., Patil, V.B., et al.: Out of order floating point co-processor for RISC V ISA. In: IEEE VLSISATA (2015)"},{"key":"41_CR36","unstructured":"Waterman, A., Lee, Y., Patterson, D.A., Asanovi, K.: The RISC-V instruction set manual. Base User-Level ISA. V2.2, vol. I (2017)"},{"key":"41_CR37","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008665528003","volume":"14","author":"E Clarke","year":"1999","unstructured":"Clarke, E., German, S.: Verifying the SRT division algorithm using theorem proving techniques. Formal Methods Syst. Des. 14, 7\u201344 (1999)","journal-title":"Formal Methods Syst. Des."},{"key":"41_CR38","doi-asserted-by":"crossref","unstructured":"Fournier, L., Arbetman, Y., et al.: Functional verification methodology for microprocessors using the genesys test program generator. Application to the x86 microprocessors family. In: DATE99 (1999)","DOI":"10.1145\/307418.307540"},{"key":"41_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/3-540-44659-1_15","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2000","unstructured":"Harrison, J.: Formal verification of IA-64 division algorithms. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 233\u2013251. Springer, Heidelberg (2000). \n                    https:\/\/doi.org\/10.1007\/3-540-44659-1_15"},{"key":"41_CR40","doi-asserted-by":"crossref","unstructured":"Jerinic, V., Langer, J., Heinkel, U., Muller, D.: New methods and coverage metrics for functional verification. In: IEEE Design, Automation and Test in Europe (2006)","DOI":"10.1109\/DATE.2006.243901"},{"key":"41_CR41","unstructured":"IEEE standards Board and ANSI. IEEE Standards for Binary Floating-point Arithmetic, IEEE Std., 754-2008 (2008)"},{"key":"41_CR42","unstructured":"Whetstone. \n                    https:\/\/www.netlib.org\/benchmark\/whetstone.c"}],"container-title":["Communications in Computer and Information Science","VLSI Design and Test"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-32-9767-8_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,12]],"date-time":"2019-09-12T02:07:09Z","timestamp":1568254029000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-981-32-9767-8_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9789813297661","9789813297678"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-981-32-9767-8_41","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"18 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VDAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on VLSI Design and Test","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Indore","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"India","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vdat2019a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/vdat2019.iiti.ac.in\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"199","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"-","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}