There exist efficient BDD circuits to verify multiplication: “Using bdds to verify multipliers,” in Proceedings of the 28th ACM/IEEE Design Automation Conference, 1991, pp. 408–412
We'll have to implement division using other primitives - addition, shifts, subtraction, etc.