Sequential equivalence checking between system level and RTL descriptions

Abraham JA, Vedula VM, Saab DG (2002) Verifying properties using sequential ATPG. In: Proceedings of the IEEE international test conference, pp 194–200

Anastasakis D, Damiano R, Ma H-KT, Stanion T (2002) A practical and efficient method for compare-point matching. In: Proceedings of the 39th design automation conference, pp 305–310

Black DC, Donovan J (2005) SystemC: From the ground up. Springer, Berlin

Burch JR, Singhal V (1998) Robust latch mapping for combinational equivalence checking. In: Proceedings of the IEEE/ACM international conference on computer-aided design, pp. 563–569

Cai L, Gajski D (2003) Transaction level modeling: an overview. In: Proceedings of the 1st IEEE/ACM/IFIP international conference on hardware/software codesign and system synthesis, pp 19–24

Calypto design systems http://www.calypto.com

Clarke E, Kroening D (2003) Hardware verification using ANSI-C programs as a reference. In: Proceedings of the IEEE Asia south pacific—Design automation conference, pp 308–311

Digital radio mondiale http://www.drm.org

Ghenassia F (ed) (2006) Transaction-level modeling with SystemC: TLM concepts and applications for embedded systems. Springer, Berlin

Fu Z, Mahajan Y, Malik S, zChaff Solver http://www.princeton.edu/~zchaff/zchaff.html

Huang S-Y, Cheng K-T, Chen K-C (2001) Verifying sequential equivalence using ATPG techniques. In: ACM transactions on design automation of electronic systems, pp 244–275

Kroening D, Clarke E, Yorav K (2003) Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of the 40th IEEE design automation conference, pp 368–371

Lu F, Iyer MK, Parthasarathy G, Wang L-C, Cheng K-T, Chen K-C (2005) An efficient sequential SAT solver with improved search strategies. In: Proceedings of the IEEE design automation and test in Europe, pp 1102–1107

Matsumoto T, Saito H, Fujita M (2005) An equivalence checking method for C descriptions based on symbolic simulation with textual differences. In: IEICE transactions on fundamentals of electronics, communications and computer sciences, pp 3315–3323

Open SystemC initiative http://www.systemc.org

Pixley C (1992) A theory and implementation of sequential hardware equivalence. In: IEEE transactions on computer-aided design of integrated circuits and systems

Pixley C (2001) Formal verification of commercial integrated circuits. In: IEEE design and test of computers

Prasad MR, Biere A, Gupta A (2005) A survey of recent advances in SAT-based formal verification. Softw Test Technol Transf (STTT) 7(2):156–173

Smria L, Mehra R, Pangrle B, Ekanayake A, Seawright A, Ng D (2002) RTL C-based methodology for designing and verifying a multi-threaded processor. In: Proceedings of the 39th design automation conference, pp 123–128

SystemC reference manual http://homes.dsi.unimi.it/~pedersin/AD/SystemC_v201_LRM.pdf

Tu J (2006) Viterbi decoder coprocessor in the DRM application SoC. Masters Report, University of Texas at Austin

van Eijk C (1998) Sequential equivalence checking without state space traversal. In: Proceedings of the IEEE design automation and test in Europe

van Eijk C, Jess J (1995) Detection of equivalent state variables in finite state machine verification. In: ACM/IEEE international workshop on logic synthesis, pp 3.35–3.44

Vasudevan S, Abraham JA, Viswanath V, Tu J (2006) Automatic decomposition for sequential equivalence checking of system level and RTL descriptions. In: Proceedings of 4th ACM-IEEE international conference on formal methods and models for codesign (MEMOCODE). IEEE, pp 71–80

Vasudevan S, Viswanath V, Sumners RW, Abraham JA (2007) Automatic verification of arithmetic circuits in RTL using stepwise refinement of term rewriting systems. IEEE Trans Comput 56(10):1401–1414

Viterbi A (1967) Error bounds for convolutional codes and an asymptotically optimum decoding algorithm. In: IEEE transactions on information theory, pp 260–269