The complexity of designs continues to rise, driven by technology advances, while time-tomarket imposes always shorter time. Moreover, the increasing of design complexity implies that design verification becomes one of the most cost-dominating phase in design production. Functional Automatic Test Pattern Generators (ATPGs) based on simulation (Corno et al., 2001; Fin & Fummi, 2003a) are fast, but generally, they are unable to cover corner cases, and they cannot prove untestability. On the contrary, functional ATPGs exploiting formal methods (Ghosh & Fujita, 2001; Zhang et al., 2003; Xin et al., 2005a), are exhaustive and cover corner cases, but they tend to suffer of the state explosion problem when adopted for verifying large designs. In this context, a functional ATPG is presented, that relies on the joint use of pseudo-deterministic simulation and constraint logic programming (CLP) (Jaffar & Maher, 1994), to generate high-quality test sequences for solving complex problems. Thus, the advantages of both simulation-based and static-based verification techniques are preserved, while their respective drawbacks are limited. In particular, CLP, a form of constraint programming in which logic programming is extended to include concepts from constraint satisfaction, is well-suited to be jointly used with simulation. In fact, information learned during design exploration by simulation can be effectively exploited for guiding the search of a CLP solver towards design under verification (DUV) areas not covered yet. Therefore, this work is focused on the use of CLP for addressing corner cases during functional test pattern generation. In particular, a CLP-based fault-oriented ATPG engine is proposed to be adopted, after simulation, learning and random-walk/backjumping, as the last step of the incremental test generation flow showed in Figure 1. According to such a flow, the ATPG framework is composed of three functional ATPG engines working on three different models of the same DUV: the hardware description language (HDL) model of the DUV, the set of concurrent EFSMs extracted from the HDL description, and the set of logic constraints modelling the EFSMs. The EFSM paradigm has been selected since it allows a compact representation of the DUV state space (Lee & Yannakakis, 1992) that limits the state explosion problem typical of more traditional FSMs. In the proposed framework, the first engine is random-based, the second is transitionoriented, while the last is fault-oriented. This approach quickly covers the greater part of DUV faults, typically easy-to-detect faults. Then, the transition-oriented engine and fault-