Novel test detection is an approach to improve simulation efficiency by selecting novel tests before their application [1]. Techniques have been proposed to apply the approach in the context of processor verification [2]. This work reports our experience in applying the approach to verifying a commercial processor. Our objectives are threefold: to implement the approach in a practical setting, to assess its effectiveness and to understand its challenges in practical application. The experiments are conducted based on a simulation environment for verifying a commercial dual-thread low-power processor core. By focusing on the complex fixed-point unit, the results show up to 96% saving in simulation time. The main limitation of the implementation is discussed based on the load-store unit with initial promising results to show how to overcome the limitation.

Ever-growing complexity is forcing design to move above RTL. For example, golden functional models are being written as clearly as possible in software and not optimized or intended for synthesis. Thus, equivalence verification between the high-level software functional model and the RTL is needed. The typical approach is to convert the high-level software into RTL or gate-level hardware, via software path enumeration, symbolic execution, or high-level synthesis techniques, and then use hardware combinational equivalence checking. The principle contribution of this paper is to introduce cutpoints --- as in gate-level combinational equivalence verification --- early during the analysis of the software model, thereby avoiding exponential path enumeration and the potential logical complexity blow-up of merging execution paths that can occur in the usual approach. The method is conservative, but in our experiments, we did not encounter spurious counterexamples, and the method showed large improvements in runtime and memory usage on a family of IA-32 subset instruction length decoders, an industry-suggested challenge problem.

With the trends toward higher-level design, verification models written in software, and hardware/software codesign, it is increasingly important to verify that RTL hardware behaves correctly according to an executable software specification. In this paper, we propose a natural way to formalize a cycle-accurate software specification as an annotated control flow graph, and then we introduce a novel partitioned model-checking algorithm that exploits the annotated control flow graph. Preliminary experimental results show that our new method runs faster than standard model checking.

Like hardware, embedded software faces stringent design constraints, undergoes extremely aggressive optimization, and therefore has a similar need for verifying the functional equivalence of two versions of a design, e.g., before and after an optimization. The concept of cutpoints was a breakthrough in the formal equivalence verification of combinational circuits and is the key enabling technology behind its successful commercialization. We introduce an analogous idea for formally verifying the equivalence of structurally similar, "combinational" software, i.e., software routines that compute a result and return/terminate, rather than executing indefinitely. We have implemented a proof-of-concept cutpoint approach in our prototype verification tool for the TI C6x family of VLIW DSPs, and our experiments show large improvements in runtime and memory usage.