More Web Proxy on the site http://driver.im/

survey

A Survey on Assertion-based Hardware Verification

Authors:

Hasini Witharana,

Subodha Charles,

Prabhat MishraAuthors Info & Claims

ACM Computing Surveys (CSUR), Volume 54, Issue 11s

Article No.: 225, Pages 1 - 33

https://doi.org/10.1145/3510578

Published: 09 September 2022 Publication History

Abstract

Hardware verification of modern electronic systems has been identified as a major bottleneck due to the increasing complexity and time-to-market constraints. One of the major objectives in hardware verification is to drastically reduce the validation and debug time without sacrificing the design quality. Assertion-based verification is a promising avenue for efficient hardware validation and debug. In this article, we provide a comprehensive survey of recent progress in assertion-based hardware verification. Specifically, we outline how to define assertions using temporal logic to specify expected behaviors in different abstraction levels. Next, we describe state-of-the art approaches for automated generation of assertions. We also discuss test generation techniques for activating assertions to ensure that the generated assertions are valid. Finally, we present both pre-silicon and post-silicon assertion-based validation approaches that utilize simulation, formal methods as well as hybrid techniques. We conclude with a discussion on utilizing assertions for verifying both functional and non-functional requirements.

References

[1]

Institute of Electrical and Electronics Engineers (IEEE). 2010. 1850-2010 - IEEE Standard for Property Specification Language (PSL). https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=5446004.

[2]

Institute of Electrical and Electronics Engineers (IEEE). 2012. 1800-2012 - IEEE Standard for SystemVerilog–Unified Hardware Design, Specification, and Verification Language. https://webstore.ansi.org/standards/ieee/ieee18002012

[3]

Open Verification Library (OVL) Working Group. 2014. Open Verification Language. Retrieved from https://www.accellera.org/downloads/standards/ovl.

[4]

Rakesh Agrawal, Tomasz Imieliński, and Arun Swami. 1993. Mining association rules between sets of items in large databases. In ACM SIGMOD Record, Vol. 22. ACM, 207–216.

[5]

Rakesh Agrawal and Ramakrishnan Srikant. 1994. Fast algorithms for mining association rules. In 20th International Conference on Very Large Data Bases, VLDB, Vol. 1215. 487–499.

[6]

Alif Ahmed, Farimah Farahmandi, and Prabhat Mishra. 2018. Directed test generation using concolic testing on RTL models. In Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1538–1543.

[7]

Alif Ahmed and Prabhat Mishra. 2017. QUEBS: Qualifying event-based search in concolic testing for validation of RTL models. In IEEE International Conference on Computer Design (ICCD’17). 185–192.

[8]

Sumit Ahuja, Deepak A. Mathaikutty, Sandeep Shukla, and Ajit Dingankar. 2007. Assertion-based modal power estimation. In 8th International Workshop on Microprocessor Test and Verification. IEEE, 3–7.

[9]

Antara Ain, Antonio Anastasio Bruto da Costa, and Pallab Dasgupta. 2016. Feature indented assertions for analog and mixed-signal validation. IEEE Trans. Comput.-Aid. Des. Integ. Circ. Syst. 35, 11 (2016), 1928–1941.

Digital Library

[10]

Ghiath Al Sammane, Mohamed H. Zaki, Zhi Jie Dong, and Sofiene Tahar. 2007. Towards assertion-based verification of analog and mixed signal designs using PSL. In Forum on Specification and Design Languages. 293–298.

[11]

Uthman Alsaiari, Fayez Gebali, and Mostafa Abd-El-Barr. 2017. Programmable assertion checkers for hardware Trojan detection. In 1st Conference on PhD Research in Microelectronics and Electronics Latin America (PRIME-LA’17). IEEE, 1–4.

[12]

Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg, Tomer Kanza, Avner Landver, Sela Mador-Haim, Eli Singerman, Andreas Tiemeyer, Moshe Vardi, and Yael Zbar. 2002. The ForSpec temporal logic: A new temporal property-specification language. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 296–311.

[13]

Viraj Athavale, Sai Ma, Samuel Hertz, and Shobha Vasudevan. 2014. Code coverage of assertions using RTL source code analysis. In 51st Annual Design Automation Conference. 1–6.

Digital Library

[14]

Kanad Basu and Prabhat Mishra. 2012. RATS: Restoration-aware trace signal selection for post-silicon validation. IEEE Trans. Very Large Scale Integ. Syst. 21, 4 (2012), 605–613.

Digital Library

[15]

Andreas Bauer and Martin Leucker. 2011. The theory and practice of SALT. In NASA Formal Methods Symposium. Springer, 13–40.

[16]

Mordechai Ben-Ari, Amir Pnueli, and Zohar Manna. 1983. The temporal logic of branching time. Acta Inform. 20, 3 (1983), 207–226.

Digital Library

[17]

Michael Bilzor, Ted Huffmire, Cynthia Irvine, and Tim Levin. 2012. Evaluating security requirements in a general-purpose processor by combining assertion checkers with code coverage. In IEEE International Symposium on Hardware-Oriented Security and Trust (HOST’12). IEEE, 49–54.

[18]

Nicola Bombieri, Riccardo Filippozzi, Graziano Pravadelli, and Francesco Stefanni. 2015. RTL property abstraction for TLM assertion-based verification. In Design, Automation & Test in Europe Conference & Exhibition. EDA Consortium, 85–90.

[19]

Nicola Bombieri, Franco Fummi, Valerio Guarnieri, Graziano Pravadelli, Francesco Stefanni, Tara Ghasempouri, Michele Lora, Giovanni Auditore, and Mirella Negro Marcigaglia. 2014. On the reuse of RTL assertions in SystemC TLM verification. In 15th Latin American Test Workshop. IEEE, 1–6.

[20]

Nicola Bombieri, Franco Fummi, Graziano Pravadelli, and Andrea Fedeli. 2007. Hybrid, incremental assertion-based verification for TLM design flows. IEEE Des. Test Comput. 24, 2 (2007).

Digital Library

[21]

Dominique Borrione, Miao Liu, Katell Morin-Allory, Pierre Ostier, and Laurent Fesquet. 2005. On-line assertion-based verification with proven correct monitors. In 3rd International Conference on Information and Communications Technology: Enabling Technologies for the New Knowledge Society. IEEE, 125–143.

[22]

Marc Boule, Jean-Samuel Chenard, and Zeljko Zilic. 2007. Assertion checkers in verification, silicon debug and in-field diagnosis. In 8th International Symposium on Quality Electronic Design. IEEE, 613–620.

[23]

Marc Boule and Zeljko Zilic. 2005. Incorporating efficient assertion checkers into hardware emulation. In IEEE International Conference on VLSI in Computers and Processors: Computer Design. IEEE, 221–228.

Digital Library

[24]

Marc Boulé and Zeljko Zilic. 2006. Efficient automata-based assertion-checker synthesis of PSL properties. In 11th IEEE International High-Level Design Validation and Test Workshop. IEEE, 69–76.

[25]

Marc Boulé and Zeljko Zilic. 2007. Efficient automata-based assertion-checker synthesis of SEREs for hardware emulation. In Asia and South Pacific Design Automation Conference. IEEE, 324–329.

Digital Library

[26]

Marc Boulé and Zeljko Zilic. 2008. Assertion checkers-enablers of quality design. In 1st Microsystems and Nanoelectronics Research Conference. IEEE, 97–100.

[27]

Marc Boulé and Zeljko Zilic. 2008. Generating Hardware Assertion Checkers. Springer.

[28]

Leonard A. Breslow and David W. Aha. 1997. Simplifying decision trees: A survey. Knowl. Eng. Rev. 12, 1 (1997), 1–40.

Digital Library

[29]

Lukai Cai and Daniel Gajski. 2003. Transaction level modeling: An overview. In 1st IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis. Association for Computing Machinery, New York, NY, 19–24. DOI:

Digital Library

[30]

Harry D. Foster. 2003. Property specification: The key to an assertion-based verification platform. Citeseer. Retrieved on April 12, 2022 fromhttp://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.134.3535.

[31]

Mingsong Chen and Prabhat Mishra. 2010. Functional test generation using efficient property clustering and learning techniques. IEEE Trans. Comput.-Aid. Des. Integ. Circ. Syst. 29, 3 (2010), 396–404.

Digital Library

[32]

Mingsong Chen and Prabhat Mishra. 2013. Assertion-based functional consistency checking between TLM and RTL models. In International Conference on VLSI Design. 320–325.

Digital Library

[33]

Mingsong Chen and Prabhat Mishra. 2013. Assertion-based functional consistency checking between TLM and RTL models. In 26th International Conference on VLSI Design and 12th International Conference on Embedded Systems. IEEE, 320–325.

Digital Library

[34]

Mingsong Chen, Prabhat Mishra, and Dhrubajyoti Kalita. 2007. Towards RTL test generation from SystemC TLM specifications. In IEEE International High Level Design Validation and Test Workshop. 91–96.

[35]

Mingsong Chen, Prabhat Mishra, and Dhrubajyoti Kalita. 2012. Automatic RTL test generation from SystemC TLM specifications. ACM Trans. Embed. Comput. Syst. 11, 2 (2012), 1–25.

Digital Library

[36]

Mingsong Chen, Xiaoke Qin, Heon-Mo Koo, and Prabhat Mishra. 2012. System-level Validation: High-level Modeling and Directed Test Generation Techniques. Springer.

Digital Library

[37]

Jean-Samuel Chenard, Stephan Bourduas, Nathaniel Azuelos, Marc Boulé, and Zeljko Zilic. 2007. Hardware assertion checkers in on-line detection of faults in a hierarchical-ring network-on-chip. In Workshop on Diagnostic Services in Network-on-Chips. 371–375.

[38]

Edmund M. Clarke. 2009. Lecture on propositional logic. Retrieved from https://www.cs.cmu.edu/emc/15414-f12/lecture/propositional-logic.pdf.

[39]

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 2000. Model Checking. The MIT Press, Cambridge, MA.

Digital Library

[40]

Silviu S. Craciunas and Ramon Serna Oliver. 2016. Combined task-and network-level scheduling for distributed time-triggered systems. Real-Time Syst. 52, 2 (2016), 161–200.

Digital Library

[41]

John Curreri, Greg Stitt, and Alan D. George. 2010. High-level synthesis techniques for in-circuit assertion-based verification. In IEEE International Symposium on Parallel & Distributed Processing, Workshops and Phd Forum (IPDPSW’10). IEEE, 1–8.

[42]

Anat Dahan, Daniel Geist, Leonid Gluhovsky, Dmitry Pidan, Gil Shapir, Yaron Wolfsthal, Lyes Benalycherif, R. Kamidem, and Younes Lahbib. 2005. Combining system level modeling with assertion -based verification. In 6th International Symposium on Quality of Electronic Design. IEEE, 310–315.

[43]

Alessandro Danese, Nicolò Dalla Riva, and Graziano Pravadelli. 2017. A-TEAM: Automatic template-based assertion miner. In 54th ACM/EDAC/IEEE Design Automation Conference (DAC’17). IEEE, 1–6.

Digital Library

[44]

Amélie David, Francois Laroussinie, and Nicolas Markey. 2016. On the expressiveness of QCTL. In 27th International Conference on Concurrency Theory (CONCUR’16) (Leibniz International Proceedings in Informatics (LIPIcs)), Josée Desharnais and Radha Jagadeesan (Eds.), Vol. 59. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 28:1–28:15. DOI:

[45]

Giuseppe Di Guglielmo, Luigi Di Guglielmo, Andreas Foltinek, Masahiro Fujita, Franco Fummi, Cristina Marconcini, and Graziano Pravadelli. 2013. On the integration of model-driven design and dynamic assertion-based verification for embedded software. J. Syst. Softw. 86, 8 (2013).

Digital Library

[46]

E. Allen Emerson and Edmund M. Clarke. 1982. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2, 3 (1982), 241–266. DOI:

[47]

Farimah Farahmandi and Prabhat Mishra. 2018. Automated test generation for debugging multiple bugs in arithmetic circuits. IEEE Trans. Comput. 68, 2 (2018), 182–197.

Digital Library

[48]

Farimah Farahmandi, Ronny Morad, Avi Ziv, Ziv Nevo, and Prabhat Mishra. 2017. Cost-effective analysis of post-silicon functional coverage events. In Design, Automation & Test in Europe Conference & Exhibition (DATE’17). IEEE, 392–397.

[49]

Andrea Fedeli, Franco Fummi, and Graziano Pravadelli. 2007. Properties incompleteness evaluation by functional verification. IEEE Trans. Comput. 56, 4 (2007), 528–544.

Digital Library

[50]

Luca Ferro, Laurence Pierre, Yves Ledru, and Lydie du Bousquet. 2008. Generation of test programs for the assertion-based verification of TLM models. In 3rd International Design and Test Workshop. IEEE, 237–242.

[51]

Harry Foster. 2012. Improving FPGA Debugging with Assertions. Retrieved from https://verificationacademy.com/news/improving-fpga-debugging-assertions.

[52]

Harry Foster. 2020. Wilson Research Group Functional Verification Study 2020. Retrievd on April 12, 2022 https://blogs.sw.siemens.com/verificationhorizons/2020/11/05/part-1-the-2020-wilson-research-group-functional-verification-study/.

[53]

Harry Foster, Kenneth Larsen, and Mike Turpin. 2006. Introduction to the new Accellera open verification library. In Design and Verification Conference and Exhibition. Citeseer.

[54]

Harry D. Foster, Adam C. Krolnik, and David J. Lacey. 2004. Assertion-based Design. Springer Science & Business Media.

Digital Library

[55]

Daniel D. Gajski, Jianwen Zhu, Rainer Dümer, Andreas Gerstlauer, and Shuqing Zhao. 2000. SPECC: Specification Language and Methodology. Springer US, Boston, MA. DOI:

[56]

Ming Gao and Kwang-Ting Cheng. 2010. A case study of time-multiplexed assertion checking for post-silicon debugging. In IEEE International High Level Design Validation and Test Workshop (HLDVT’10). IEEE, 90–96.

[57]

Frank Ghenassia (Ed.). 2005. Transaction Level Modeling with SystemC. Springer US. DOI:

[58]

John Havlicek and Scott Little. 2011. Realtime regular expressions for analog and mixed-signal assertions. In Formal Methods in Computer-Aided Design (FMCAD’11). IEEE, 155–162.

[59]

Amir Hekmatpour and Azadeh Salehi. 2005. Block-based schema-driven assertion generation for functional verification. In 14th Asian Test Symposium. IEEE, 34–39.

[60]

Samuel Hertz, David Sheridan, and Shobha Vasudevan. 2013. Mining hardware assertions with guidance from static analysis. IEEE Trans. Comput.-Aid. Des. Integ. Circ. Syst. 32, 6 (2013), 952–965.

Digital Library

[61]

Nikhil Jayakumar, Mitra Purandare, and Fabio Somenzi. 2003. Do’s and don’ts of CTL state coverage estimation. In Design Automation Conference. IEEE, 292–295.

[62]

Alexander Jesser, Stefan Laemmermann, A. Pacholik, R. Weiss, Juergen Ruf, W. Fengler, L. Hedrich, T. Kropf, and Wolfgang Rosenstiel. 2007. Analog simulation meets digital verification–A formal assertion approach for mixed-signal verification. In SASIMI, Vol. 7. 507–514.

[63]

Mohammad Reza Kakoee, Mohammad Hossein Neishaburi, Masoud Daneshtalab, Saeed Safari, and Zainalabedin Navabi. 2007. On-chip verification of NoCs using assertion processors. In 10th Euromicro Conference on Digital System Design Architectures, Methods and Tools (DSD’07). IEEE, 535–538.

Digital Library

[64]

Vivek N. Kallankara, M. H. Neishaburi, Katarzyna Radecka, and Zeljko Zilic. 2010. Using assertions for wireless system monitoring and debugging. In 8th IEEE International NEWCAS Conference (NEWCAS’10). IEEE, 401–404.

[65]

Michael Katrowitz and Lisa M. Noack. 1996. I’m done simulating; now what? Verification coverage analysis and correctness checking of the DEC chip 21164 Alpha microprocessor. In 33rd Annual Design Automation Conference. ACM, 325–330.

Digital Library

[66]

Steve Kerrison, David May, and Kerstin Eder. 2016. A Benes-based NoC switching architecture for mixed criticality embedded systems. In IEEE 10th International Symposium on Embedded Multicore/Many-core Systems-on-chip (MCSOC’16). IEEE, 125–132.

[67]

Alexander Knüppel, Leon Schaer, and Ina Schaefer. 2021. How much specification is enough? Mutation analysis for software contracts. In IEEE/ACM 9th International Conference on Formal Methods in Software Engineering (FormaliSE’21). IEEE, 42–53.

[68]

Heon-Mo Koo and Prabhat Mishra. 2009. Functional test generation using design and property decomposition techniques. ACM Trans. Embed. Comput. Syst. 8, 4 (2009), 1–33.

Digital Library

[69]

Bogdan Korel and Ali M. Al-Yami. 1996. Assertion-oriented automated test data generation. In 18th International Conference on Software Engineering. IEEE Computer Society, 71–80.

Digital Library

[70]

Yangyang Li, Wuchen Wu, Ligang Hou, and Hao Cheng. 2009. A study on the assertion-based verification of digital IC. In 2nd International Conference on Information and Computing Science. IEEE, 25–28.

Digital Library

[71]

Lingyi Liu, Chen-Hsuan Lin, and Shobha Vasudevan. 2012. Word level feature discovery to enhance quality of assertion mining. In IEEE/ACM International Conference on Computer-Aided Design (ICCAD’12). IEEE, 210–217.

Digital Library

[72]

Lingyi Liu, David Sheridan, Viraj Athavale, and Shobha Vasudevan. 2011. Automatic generation of assertions from system level design using data mining. In 9th ACM/IEEE International Conference on Formal Methods and Models for Codesign. IEEE Computer Society, 191–200.

Digital Library

[73]

Yangdi Lyu, Alif Ahmed, and Prabhat Mishra. 2019. Automated activation of multiple targets in RTL models using concolic testing. In Design, Automation & Test in Europe Conference & Exhibition (DATE’19). IEEE, 354–359.

[74]

Yangdi Lyu and Prabhat Mishra. 2020. Automated test generation for activation of assertions in RTL models. In 25th Asia and South Pacific Design Automation Conference (ASP-DAC’20). IEEE, 223–228.

Digital Library

[75]

Yangdi Lyu and Prabhat Mishra. 2020. Scalable concolic testing of RTL models. IEEE Trans. Comput. 70, 7 (2020), 979–991.

[76]

Yangdi Lyu, Xiaoke Qin, Mingsong Chen, and Prabhat Mishra. 2018. Directed test generation for validation of cache coherence protocols. IEEE Trans. Computer-Aid. Des. Integ. Circ. Syst. 38, 1 (2018), 163–176.

Digital Library

[77]

Kenneth L. McMillan. 1993. The SMV system. In Symbolic Model Checking. Springer, 61–85.

[78]

Ashok B. Mehta. 2018. Analog/mixed signal (AMS) verification. In ASIC/SoC Functional Design Verification. Springer, 255–271.

[79]

Ashok B. Mehta. 2020. System Verilog assertions. In System Verilog Assertions and Functional Coverage. Springer, 11–31.

[80]

Prabhat Mishra and Farimah Farahmandi. 2019. Post-Silicon Validation and Debug. Springer.

[81]

Wolfgang Mueller, Marcio F. da S. Oliveira, Henning Zabel, and Markus Becker. 2010. Verification of real-time properties for hardware-dependent software. In IEEE International High Level Design Validation and Test Workshop (HLDVT’10). IEEE, 154–159.

[82]

R. Mukherjee, D. Kroening, and T. Melham. 2015. Hardware verification using software analyzers. In IEEE Computer Society Annual Symposium on VLSI. IEEE, 7–12. DOI:

[83]

Mohammad Hossein Neishaburi and Zeljko Zilic. 2010. Enabling efficient post-silicon debug by clustering of hardware-assertions. In Design, Automation & Test in Europe Conference & Exhibition (DATE’10). IEEE, 985–988.

[84]

Mohammad Hossein Neishaburi and Zeljko Zilic. 2012. An infrastructure for debug using clusters of assertion-checkers. Microelectron. Reliab. 52, 11 (2012), 2781–2798.

[85]

Antti Pakonen, Cheng Pang, Igor Buzhinsky, and Valeriy Vyatkin. 2016. User-friendly formal specification languages-conclusions drawn from industrial experience on model checking. In IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA’16). IEEE, 1–8.

Digital Library

[86]

Bhaskar Pal, Ansuman Banerjee, Arnab Sinha, and Pallab Dasgupta. 2008. Accelerating assertion coverage with adaptive testbenches. IEEE Trans. Comput.-Aid. Des. Integ. Circ. Syst. 27, 5 (2008), 967–972.

Digital Library

[87]

Michael Pellauer, Mieszko Lis, Don Baltus, and Rishiyur Nikhil. 2005. Synthesis of synchronous assertions with guarded atomic actions. In 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE’05). IEEE, 15–24.

Digital Library

[88]

A. Pnueli. 1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (SFCS’77). 46–57. DOI:

Digital Library

[89]

Xiaoke Qin and Prabhat Mishra. 2012. Directed test generation for validation of multicore architectures. ACM Trans. Des. Autom. Electron. Syst. 17, 3 (2012), 1–21.

Digital Library

[90]

Xiaoke Qin, Weixun Wang, and Prabhat Mishra. 2012. TCEC: Temperature and energy-constrained scheduling in real-time multitasking systems. IEEE Trans. Comput.-Aid. Des. Integ. Circ. Syst. 31, 8 (2012), 1159–1168.

Digital Library

[91]

Kamran Rahmani and Prabhat Mishra. 2017. Feature-based signal selection for post-silicon debug using machine learning. IEEE Trans. Emerg. Topics Comput. 8, 4 (2017), 907–915.

[92]

Kamran Rahmani, Sudhi Proch, and Prabhat Mishra. 2015. Efficient selection of trace and scan signals for post-silicon debug. IEEE Trans. Very Large Scale Integ. Syst. 24, 1 (2015), 313–323.

Digital Library

[93]

Kamran Rahmani, Sandip Ray, and Prabhat Mishra. 2016. Postsilicon trace signal selection using machine learning techniques. IEEE Trans. Very Large Scale Integ. Syst. 25, 2 (2016), 570–580.

Digital Library

[94]

Zhihong Ren and Hussain Al-Asaad. 2016. Overview of assertion-based verification and its applications. In International Conference on Embedded Systems, Cyber-physical Systems, & Applications.

[95]

Aurélien Ribon, Bertrand Le Gal, Christophe Jégo, and Dominique Dallet. 2011. Assertion support in high-level synthesis design flow. In Forum on Specification and Design Languages (FDL’11). IEEE, 1–8.

[96]

S. Savithri, R. Venkatesan, and S. Bhaskar. 2000. An assertion-based technique for transistor level dynamic power estimation. In 13th International Conference on VLSI Design: Wireless and Digital Imaging in the Millennium. IEEE, 34–37.

[97]

David Sheridan, Lingyi Liu, Hyungsul Kim, and Shobha Vasudevan. 2014. A coverage guided mining approach for automatic generation of succinct assertions. In 27th International Conference on VLSI Design and 13th International Conference on Embedded Systems. IEEE, 68–73.

Digital Library

[98]

Pouya Taatizadeh and Nicola Nicolici. 2015. Emulation-based selection and assessment of assertion checkers for post-silicon validation. In 33rd IEEE International Conference on Computer Design (ICCD’15). IEEE, 46–53.

Digital Library

[99]

Pouya Taatizadeh and Nicola Nicolici. 2016. Automated selection of assertions for bit-flip detection during post-silicon validation. IEEE Trans. Comput.-Aid. Des. Integ. Circ. Syst. 35, 12 (2016), 2118–2130.

Digital Library

[100]

Pouya Taatizadeh and Nicola Nicolici. 2017. Emulation infrastructure for the evaluation of hardware assertions for post-silicon validation. IEEE Trans. Very Large Scale Integ. Syst. 25, 6 (2017), 1866–1880.

Digital Library

[101]

Deian Tabakov, Gila Kamhi, Moshe Y. Vardi, and Eli Singerman. 2008. A temporal language for SystemC. In Formal Methods in Computer-Aided Design (FMCAD’08). IEEE, 1–9.

[102]

Jimmy Tarrillo, Letícia Maria Bolzani Pohls, and Fabian Vargas. 2009. A hardware-scheduler for fault detection in RTOS-based embedded systems. In 12th Euromicro Conference on Digital System Design, Architectures, Methods and Tools. IEEE, 341–347.

Digital Library

[103]

Jason G. Tong, Marc Boulé, and Zeljko Zilic. 2009. Airwolf-TG: A test generator for assertion-based dynamic verification. In IEEE International High Level Design Validation and Test Workshop. IEEE, 106–113.

[104]

Jason G. Tong, Marc Boulé, and Zeljko Zilic. 2013. Test compaction techniques for assertion-based test generation. ACM Trans. Des. Autom. Electron. Syst. 19, 1 (Dec. 2013). DOI:

Digital Library

[105]

Babu Turumella and Mukesh Sharma. 2008. Assertion-based verification of a 32 thread SPARC™ CMT microprocessor. In 45th ACM/IEEE Design Automation Conference. IEEE, 256–261.

[106]

Shobha Vasudevan, David Sheridan, Sanjay Patel, David Tcheng, Bill Tuohy, and Daniel Johnson. 2010. GoldMine: Automatic assertion generation using data mining and static analysis. In Conference on Design, Automation and Test in Europe. European Design and Automation Association, 626–629.

[107]

D. S. Vidhya and Manjunath Ramachandra. 2017. A novel design in formal verification corresponding to mixed signals by differential learning. In Computer Science On-line Conference. Springer, 367–378.

[108]

Hanbo Wang, Xingshe Zhou, Yunwei Dong, and Lei Tang. 2010. Timing properties analysis of real-time embedded systems with AADL model using model checking. In IEEE International Conference on Progress in Informatics and Computing. IEEE, 1019–1023.

[109]

Hasini Witharana, Yangdi Lyu, and Prabhat Mishra. 2020. Directed test generation for activation of security assertions in RTL models. ACM Trans. Des. Autom. Electron. Syst.

[110]

Takamitsu Yamada. 2009. Assertion generating system, program thereof, circuit verifying system, and assertion generating method. US Patent 7,603,636.

Cited By

Qin MLi JYan JHao ZHu WLiu B(2024)HT-PGFV: Security-Aware Hardware Trojan Security Property Generation and Formal Security Verification SchemeElectronics10.3390/electronics1321428613:21(4286)Online publication date: 31-Oct-2024
https://doi.org/10.3390/electronics13214286
Sanjaya SWitharana HMishra P(2024)Assertion-Based Validation using Clustering and Dynamic Refinement of Hardware CheckersACM Transactions on Design Automation of Electronic Systems10.1145/369610829:6(1-22)Online publication date: 16-Sep-2024
https://dl.acm.org/doi/10.1145/3696108
Akyash MM Kamali H(2024)Evolutionary Large Language Models for Hardware Security: A Comparative SurveyProceedings of the Great Lakes Symposium on VLSI 202410.1145/3649476.3660390(496-501)Online publication date: 12-Jun-2024
https://dl.acm.org/doi/10.1145/3649476.3660390
Show More Cited By

Index Terms

A Survey on Assertion-based Hardware Verification
1. Hardware
  1. Hardware validation
    1. Functional verification
      1. Assertion checking
    2. Post-manufacture validation and debug
      1. Bug detection, localization and diagnosis

Recommendations

Formal verification in hardware design: a survey

In recent years, formal methods have emerged as an alternative approach to ensuring the quality and correctness of hardware designs, overcoming some of the limitations of traditional validation techniques such as simulation and testing.

There are two ...
Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers
Tools and Algorithms for the Construction and Analysis of Systems
Abstract
Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the confidence in verification results by generating a witness for other tools to validate the verdict ...
Formal hardware verification methods: a survey
Special issue on computer-aided verification: general methods

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Computing Surveys

ACM Computing Surveys Volume 54, Issue 11s

January 2022

785 pages

ISSN:0360-0300

EISSN:1557-7341

DOI:10.1145/3551650

Editor:
Albert Zomaya
University of Sydney, Australia

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 September 2022

Online AM: 28 January 2022

Accepted: 01 January 2022

Revised: 01 January 2022

Received: 01 April 2021

Published in CSUR Volume 54, Issue 11s

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Survey
Refereed

Funding Sources

National Science Foundation
Semiconductor Research Corporation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
Total Citations
View Citations
1,834
Total Downloads

Downloads (Last 12 months)795
Downloads (Last 6 weeks)80

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Qin MLi JYan JHao ZHu WLiu B(2024)HT-PGFV: Security-Aware Hardware Trojan Security Property Generation and Formal Security Verification SchemeElectronics10.3390/electronics1321428613:21(4286)Online publication date: 31-Oct-2024
https://doi.org/10.3390/electronics13214286
Sanjaya SWitharana HMishra P(2024)Assertion-Based Validation using Clustering and Dynamic Refinement of Hardware CheckersACM Transactions on Design Automation of Electronic Systems10.1145/369610829:6(1-22)Online publication date: 16-Sep-2024
https://dl.acm.org/doi/10.1145/3696108
Akyash MM Kamali H(2024)Evolutionary Large Language Models for Hardware Security: A Comparative SurveyProceedings of the Great Lakes Symposium on VLSI 202410.1145/3649476.3660390(496-501)Online publication date: 12-Jun-2024
https://dl.acm.org/doi/10.1145/3649476.3660390
Miftah SSrivastava AKim HBasu K(2024)Assert-O: Context-based Assertion Optimization using LLMsProceedings of the Great Lakes Symposium on VLSI 202410.1145/3649476.3660378(233-239)Online publication date: 12-Jun-2024
https://dl.acm.org/doi/10.1145/3649476.3660378
Jayasena AMishra P(2024)Directed Test Generation for Hardware Validation: A SurveyACM Computing Surveys10.1145/363804656:5(1-36)Online publication date: 12-Jan-2024
https://dl.acm.org/doi/10.1145/3638046
Kande RGohil VDeLorenzo MChen CRajendran J(2024)LLMs for Hardware Security: Boon or Bane?2024 IEEE 42nd VLSI Test Symposium (VTS)10.1109/VTS60656.2024.10538871(1-4)Online publication date: 22-Apr-2024
https://doi.org/10.1109/VTS60656.2024.10538871
Kande RPearce HTan BDolan-Gavitt BThakur SKarri RRajendran J(2024)(Security) Assertions by Large Language ModelsIEEE Transactions on Information Forensics and Security10.1109/TIFS.2024.337280919(4374-4389)Online publication date: 4-Mar-2024
https://dl.acm.org/doi/10.1109/TIFS.2024.3372809
Witharana HWeerasena HMishra P(2024)Formal Verification of Virtualization-Based Trusted Execution EnvironmentsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.344300843:11(4262-4273)Online publication date: Nov-2024
https://doi.org/10.1109/TCAD.2024.3443008
Miftah SRaj KMeng XRay SBasu K(2024)System-on-Chip Information Flow Validation Under Asynchronous ResetsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.337659643:9(2825-2838)Online publication date: 13-Mar-2024
https://dl.acm.org/doi/10.1109/TCAD.2024.3376596
Iman MAhmadi-Pour SDrechsler RGhasempouri T(2024)Processor Vulnerability Detection with the Aid of Assertions: RISC-V Case Study2024 IEEE Nordic Circuits and Systems Conference (NorCAS)10.1109/NorCAS64408.2024.10752460(1-7)Online publication date: 29-Oct-2024
https://doi.org/10.1109/NorCAS64408.2024.10752460
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Full Text

View this article in Full Text.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View full text|Download PDF

View Issue’s Table of Contents