An Efficient Rewriting Framework for Trace Coverage of Symmetric Systems
Verification coverage is an important metric in any hardware verification effort. Coverage models are proposed as a set of events the hardware may exhibit, intended to be possible under a test scenario. At the system level, these events each correspond to a visited state or taken transition in a transition system that represents the underlying hardware. A more sophisticated approach is to check that tests exercise specific sequences of events, corresponding to traces through the transition system. However, such trace-based coverage models are inherently expensive to consider in practice, as the number of traces is exponential in trace length. We present a novel framework that combines the approaches of conservative abstraction with rewriting to construct a concise trace-based coverage model of a class of parameterized symmetric systems. First, we leverage both symmetry and rewriting to construct abstractions that can be tailored by users’ defined rewriting. Then, under this abstraction, a coverage model for a larger system can be generated from traces for a smaller system. This coverage model is of tractable size, is tractable to generate, and can be used to identify coverage-holes in large systems. Our experiments on the cache coherence protocol implementation from the multi-billion transistors IBM POWER™ Processor demonstrate the viability and effectiveness of this approach.
The authors thank Viresh Paruthi and Jesse Bingham for valuable suggestions that helped with clarity of this paper.
- 2.Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411–420. IEEE (1999)Google Scholar
- 4.Ziv, A.: Cross-product functional coverage measurement with temporal properties-based assertions. In: DATE, p. 10834. IEEE (2003)Google Scholar
- 7.Czemerinski, H., Braberman, V., Uchitel, S.: Behaviour abstraction coverage as black-box adequacy criteria. In: ICST, pp. 222–231. IEEE (2013)Google Scholar
- 8.Castillos, K.C., Dadeau, F., Julliand, J.: Coverage criteria for model-based testing using property patterns. In: Proceedings of 9th MBT Workshop, pp. 29–43 (2014)Google Scholar
- 9.Papamarcos, M.S., Patel, J.H.: A low-overhead coherence solution for multiprocessors with private cache memories. In: Proceedings of 11th Annual International Symposium on Computer Architecture, pp. 348–354. ACM, New York (1984)Google Scholar
- 11.Chou, Ching-Tsun, Mannava, Phanindra K., Park, Seungjoon: A simple method for parameterized verification of cache coherence protocols. In: Hu, Alan J., Martin, Andrew K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382–398. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30494-4_27 CrossRefGoogle Scholar
- 16.Cragon, H.G.: Memory Systems and Pipelined Processors. Jones and Bartlett Publishers, Burlington (1996)Google Scholar
- 17.Shimizu, K., et. al.: Verification of the cell broadband engine; processor. In: Proceedings of 43rd Annual DAC, pp. 338–343. ACM (2006)Google Scholar