This paper presents a testable synthesis methodology applicable to any top-down design method based on hardware-description-language descriptions, or graphical representations. The methodology is targeted on control-dominated applications and it is based on the identification and removal of a new class of redundant faults, called functionally redundant faults. The formal relation between functionally redundant faults and sequentially redundant faults is introduced. Moreover, the relation between functionally redundant faults and logic synthesis algorithms based on local don't cares is shown. Functionally redundant faults are identified and removed by comparing the implemented synchronous sequential circuit, which can be technology dependent...