RTL SAT simplification by Boolean and interval arithmetic reasoning

We present a method that combines interval-arithmetic (IA) and Boolean reasoning with structural hashing for simplifying SAT problems on circuits expressed at the register-transfer level. We demonstrate that simple transformations based on interval-arithmetic operations can significantly reduce the complexity of the problem. We identify cases where the inherent over-approximations in IA operations can be reduced. We demonstrate that these techniques can significantly reduce RTL-SAT instances in size and runtime.