Abstract
Semiconductor companies have increasingly adopted a methodology that starts with a system-level design specification in C/C++/SystemC. This model is extensively simulated to ensure correct functionality and performance. Later, a Register Transfer Level (RTL) implementation is created in Verilog, either manually by a designer or automatically by a high-level synthesis tool. It is essential to check that the C and Verilog programs are consistent. In this paper, we present a two-step approach, embodied in two equivalence checking tools, VerifOx and hw-cbmc, to validate designs at the software and RTL levels, respectively. VerifOx is used for equivalence checking of an untimed software model in C against a high-level reference model in C. hw-cbmc verifies the equivalence of a Verilog RTL implementation against an untimed software model in C. To evaluate our tools, we applied them to a commercial floating-point arithmetic unit (FPU) from ARM and an open-source dual-path floating-point adder.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
- 3.
The SAT community uses the term assumption variables or assumptions, but we will use the term blocking variable to avoid ambiguity with assumptions in the program.
- 4.
References
Baumgartner, J., Mony, H., Paruthi, V., Kanzelman, R., Janssen, G.: Scalable sequential equivalence checking across arbitrary design transformations. In: ICCD, pp. 259–266. IEEE (2006)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003)
Brand, D.: Verification of large synthesized designs. In: ICCAD, pp. 534–537 (1993)
Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209–224. USENIX (2008)
Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. 12(2), 10:1–10:38 (2008). Article No.10
Clarke, E., Kroening, D.: Hardware verification using ANSI-C programs as a reference. In: Proceedings of the 2003 Asia and South Pacific Design Automation Conference, ASP-DAC, pp. 308–311. ACM (2003)
Clarke, L.A.: A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2(3), 215–222 (1976)
Collingbourne, P., Cadar, C., Kelly, P.H.J.: Symbolic crosschecking of floating-point and SIMD code. In: EuroSys, pp. 315–328 (2011)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: An efficient method of computing static single assignment form. In: POPL, pp. 25–35. ACM (1989)
Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005). doi:10.1007/11499107_5
van Eijk, C.A.J.: Sequential equivalence checking without state space traversal. In: DATE, pp. 618–623. IEEE (1998)
Fujita, M.: Verification of arithmetic circuits by comparing two similar circuits. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 159–168. Springer, Heidelberg (1996). doi:10.1007/3-540-61474-5_66
Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: PLDI, pp. 213–223 (2005)
Kölbl, A., Jacoby, R., Jain, H., Pixley, C.: Solver technology for system-level to RTL equivalence checking. In: DATE, pp. 196–201. IEEE (2009)
Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: DAC, pp. 368–371 (2003)
Kuznetsov, V., Kinder, J., Bucur, S., Candea, G.: Efficient state merging in symbolic execution. In: PLDI, pp. 193–204 (2012)
Mukherjee, R., Joshi, S., Griesmayer, A., Kroening, D., Melham, T.: Equivalence checking a floating-point unit against a high-level C model: extended version. Computing Research Repository arXiv:1609.00169 [cs.SE], September 2016
Wu, W., Hsiao, M.S.: Mining global constraints for improving bounded sequential equivalence checking. In: DAC, pp. 743–748. ACM (2006)
Xue, B., Chatterjee, P., Shukla, S.K.: Simplification of C-RTL equivalent checking for fused multiply add unit using intermediate models. In: ASP-DAC, pp. 723–728. IEEE (2013)
Acknowledgements
Part of the presented work was conducted during an internship at ARM. The authors want to thank in particular Luka Dejanovic, Joe Tapply, and Ian Clifford for their help with setting up the experiments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Mukherjee, R., Joshi, S., Griesmayer, A., Kroening, D., Melham, T. (2016). Equivalence Checking of a Floating-Point Unit Against a High-Level C Model. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_33
Download citation
DOI: https://doi.org/10.1007/978-3-319-48989-6_33
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-48988-9
Online ISBN: 978-3-319-48989-6
eBook Packages: Computer ScienceComputer Science (R0)