FPGA-Assisted Assertion-Based Verification Platform
Keywords:
Arbitration, Assertion-based Verification, Assertion checker, FPGA, System Verilog Assertion, Verilog.Abstract
In this paper, field programmable gate array (FPGA)-assisted verification platform is devised to enhance the assertion-based verification methodology to address the issues of high demand of integrated circuit with the advanced features to be delivered to market within tight Time-To-Market. The concept of SystemVerilog Assertion (SVA) checker generator is introduced to translate non-synthesizable verification coding into hardware so-called assertion checker in Verilog. A lookup table, which comprises of SVA operators mapped to their corresponding synthesizable Verilog coding was developed to generate assertion checker, which produces a single bit 1 when the assertion fails. Collection module implemented using a memory block and an arbiter was devised to be simple and fast enough to collect assertion results from the assertion checker. Since assertion checker can produce assertion result at any time, an arbiter is required to act as an interface between assertion checker and collection module. Case studies have been conducted on the proof-of-concept designs, which are the firstin-first-out (FIFO), up-down counter and Context Adaptive Variable Length Coding (CAVLC) to evaluate the effectiveness of the proposed FPGA-assisted verification platform. In the case studies, we have shown that the proposed FPGA-assisted verification platform works correctly. Besides, we also evaluated the method in area utilizations (ALMs). It has been proven that simulation-based verification time can be reduced for as much as 50% for complexity of VLSI design. Thus, implementing assertions using hardware such as FPGA becomes a solution to alleviate issue of long simulation time.References
Foster HD. Trends in Functional Verification : A 2014 Industry Study 2015.
Kuznik Ct, Mueller W, Le HM, Große D, Drechsler R. The System Verification Methodology for Advanced TLM Verification Categories and Subject Descriptors, 2011, pp. 313–322.
Bamford N, Bangalore RK, Chapman E, Chavez H, Dasari R, Lin Y, et al. "Challenges in System on Chip Verification," Seventh International Workshop on Microprocessor Test and Verification, 2006, pp. 52–60.
Boulâe M, Zilic Z. Generating hardware assertion checkers. Montreal: Springer Science + Business Media B.V, 2008.
Foster H, Krolnik A, Lacey D. Assertion-based design. Boston: Kluwer Academic Publisher, 2005.
Hutchison D, Mitchell JC. Formal Methods for Hardware Verification. Germany: Springer, 2006.
Pierre L, Pancher F, Suescun R, Quévremont J, "On the effectiveness of assertion-based verification in an industrial context," Proceedings of the 18th International Workshop on Formal Methods for Industrial Critical Systems, Volume 8187, New York, NY, USA: Springer-Verlag New York, Inc, 2013.
Abarbanel Y, Beer I, Gluhovsky L, Keidar S, "FoCs: automatic generation of simulation checkers from formal specifications," Proc. 12th International Conference on computer aided verification, 2000.
Foster H, Assertion-based verification: Industry myths to realities (invited tutorial). Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2008, pp. 5–10.
Bombieri N, Fummi F, Guarnieri V, Pravadelli G, Stefanni F, Ghasempouri T, et al, "On the reuse of RTL assertions," in SystemC TLM verification, 2014.
Šimková M, Lengál O, Kajan M. HAVEN, An open framework for FPGA-accelerated functional verification of hardware. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 2012, pp. 247–253.
Boul M, Chenard J samuel, Zilic Z, Assertion Checkers in Verification, Silicon Debug and In-Field Diagnosis 2007.
Lu Y, Zhu Y, Assertion Synthesis : Enabling Assertion-Based Verification For Simulation, Formal and Emulation Flows, pp. 1–7.
Das S, Mohanty R, Dasgupta P, Chakrabarti PP, "Synthesis of system verilog assertions," Proceedings-Design, Automation and Test in Europe, DATE 2006, pp. 70–75.
Chuang C. Lung, Liu C Nan J, "Hybrid Testbench Acceleration for Reducing Communication Overhead," 2011, pp. 40–51.
Boul M, Zilic Z, "Incorporating efficient assertion checkers into hardware emulation," Proceedings of the 2005 International Conference on Computer Design (ICCD’05), 2005.
Koczor A, Matoga L, Penkala P, Pawlak A, "Verification approach based on emulation technology," Proceedings of the 2016 IEEE 19th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, 2016.
Tomas BJ, Jiang Y, Yang M, "SoC Scan-Chain verification utilizing FPGA-based emulation platform and SCE-MI interface," International System on Chip Conference 2014, pp. 398–403.
Tong JG, Boulé M, Zilic Z, "Test compaction techniques for assertionbased test generation," ACM Transactions on Design Automation of Electronic Systems, 2013.
Bailey B, Martin G, Arderson T, Taxonomies for the Development and Verification of Digital Systems, United States: Springer Science + Business Media B.V, 2005.
Li Y, Wu W, Hou L, Cheng H, "A study on the assertion-based verification of digital IC," International Conference on Information and Computing Science, 2009, pp. 25–28.
Boulé M, Zilic Z, "Automata-based assertion-checker synthesis of PSL properties," ACM Transactions on Design Automation of Electronic Systems, 2008.
Pellauer M, Lis M, Baltus D, Nikhil R, Synthesis of Synchronous Assertions with Guarded Atomic Actions, 2005.
Sonny AT, OVL, PSL, SVA : Assertion Based Verification Using Checkers and Standard Assertion Languages.
Kumar Tala D. World of Asic 2014. http://www.asicworld.com/systemverilog/operators.html.
Downloads
Published
How to Cite
Issue
Section
License
TRANSFER OF COPYRIGHT AGREEMENT
The manuscript is herewith submitted for publication in the Journal of Telecommunication, Electronic and Computer Engineering (JTEC). It has not been published before, and it is not under consideration for publication in any other journals. It contains no material that is scandalous, obscene, libelous or otherwise contrary to law. When the manuscript is accepted for publication, I, as the author, hereby agree to transfer to JTEC, all rights including those pertaining to electronic forms and transmissions, under existing copyright laws, except for the following, which the author(s) specifically retain(s):
- All proprietary right other than copyright, such as patent rights
- The right to make further copies of all or part of the published article for my use in classroom teaching
- The right to reuse all or part of this manuscript in a compilation of my own works or in a textbook of which I am the author; and
- The right to make copies of the published work for internal distribution within the institution that employs me
I agree that copies made under these circumstances will continue to carry the copyright notice that appears in the original published work. I agree to inform my co-authors, if any, of the above terms. I certify that I have obtained written permission for the use of text, tables, and/or illustrations from any copyrighted source(s), and I agree to supply such written permission(s) to JTEC upon request.
