Automated detection and verification of parity-protected memory elements

With technology scaling and complexity, better error detection and correction mechanisms within chips and systems are becoming increasingly important in order to provide sufficient protection against both soft and hard errors. Verifying the correctness of error detection circuits and ensuring they provide enough design coverage is a hard problem which usually involves substantial amount of manual work. This problem is even more challenging in the presence of different design methodologies, such as with the inclusion of third party IP blocks where functional descriptions of logic designs may not be available. This paper addresses the problem by proposing a completely automated RTL-based verification flow for error detection and correction circuits. Several related challenges are solved: first, that of identification of potential error detection circuits in logic designs where no functional description or methodology hints are given. Second, identification of structures of the latches that are potentially protected by such error detection circuits. Third, using formal verification for ensuring that the implemented circuits for resiliency indeed detect all single bit errors in the latches they are intended to cover. The approach is described with parity detection as an example, although it is extensible to other coding methods such as ECC and state orthogonality checking. Novel algorithms are given and results on industrial designs are presented.