A formal behavioral test generation algorithm, called the B-algorithm, is presented together with a behavioral VHDL model and a realistic behavioral fault model. Using the behavioral VHDL model, a behavioral VHDL circuit description is represented as a set of equivalent process Statements and connections among them. The behavioral fault model consists of three types of behavioral faults (behavioral stuck-at faults, behavioral stuck-open faults, and micro-operation faults) which well represent faulty behaviors of a digital circuit. The behavioral VHDL model and the behavioral fault model improve the efficiency of test generation by reducing the size of the domain searched during the test generation procedure. The B-algorithm generates tests directly from behavioral VHDL circuit descriptions using three basic test generation operations (activation, propagation, and justification), which are systematically executed by manipulating three data structures (B-frontier, J-frontier, and A-queue). Rules for the test generation operations are formally defined using the concepts of two-phase activation and two-phase propagation. The difference between simulation semantics and test generation semantics is discussed, and a method of efficiently assigning time periods without being affected by simulation semantics is proposed. A method of handling bus resolution functions, reconvergent fanout, and feedback loops during test generation is discussed. Two-phase testing, a testing strategy where a fault is detected using two consecutive test sequences, is introduced and 1s formally incorporated into the B-algorithm. / Ph. D.