Optimized and custom arithmetic circuits are widely used in embedded systems such as multimedia applications, cryptography systems, signal processing, and console games. Verification of arithmetic circuits is a challenge due to increasing complexity coupled with non-standard implementations. Existing algebraic rewriting techniques produce a remainder to indicate the presence of a potential Trojan. However, Trojan localization remains a major bottleneck. Simulation-based validation using random or constrained-random tests is not effective for complex arithmetic circuits due to bit-blasting. In this chapter, we present an automated test generation and Trojan localization technique for arithmetic circuits. We consider gate-replacement Trojan or signal inversion that changes the functionality of the design as the threat model. In this chapter, we present an automated approach for generating directed tests by suitable assignments of input variables to make the remainder non-zero. The generated tests are guaranteed to activate Trojans. We also present an automatic Trojan removal technique by utilizing the patterns of the remainder terms as well as by analyzing the regions activated by the generated tests to detect and correct the Trojan(s). We also present an efficient anomaly detection and correction algorithm that can handle multiple dependent as well as independent Trojans. This framework is capable of producing a corrected implementation of arithmetic circuits without any manual intervention. The experimental results demonstrate that the proposed approach can be used for automated anomaly detection and correction of large and complex arithmetic circuits.