With the increase of device complexity and test-data volume required to guarantee adequate defect coverage, external testing is becoming increasingly difficult and expensive. Logic Built-in Self Test (LBIST) is a viable alternative test strategy as it helps reduce dependence on an elaborate external test equipment, enables the application of a large number of random tests, and allows for at-speed testing. The main problem with LBIST is suboptimal fault coverage achievable with random vectors. LFSR reseeding is used to increase the coverage. However, to achieve satisfactory coverage, one often needs a large number of seeds. Computing a small number of seeds for LBIST reseeding still remains a tremendous challenge, since the vectors needed to detect all faults may be spread across the huge LFSR vector space. In this work, we propose new methods to enable the computation of a small number of LFSR seeds to cover all stuck-at faults as a first-order satisfiability problem involving extended theories. We present a technique based on SMT (Satisfiability Modulo Theories) with the theory of bit-vectors to combine the tasks of test-generation and seed computation. We describe a seed reduction flow which is based on the `chaining' of faults instead of pre-computed vectors. We experimentally demonstrate that our method can produce very small sets of seeds for complete stuck-at fault coverage. Additionally, we present methods for inserting test-points to enhance the testability of a circuit in such a way as to allow even further reduction in the number of seeds. / Master of Science