Polynomial Formal Verification (PFV) is considered as a specific class of formal verification methodology that targets verification within space and time limits. Several works have already focused on PFV of arithmetic circuits and processors. PFV of processors, as reported in recent work, only considers the base instruction set, but no multiplier units were taken into account. In this paper, we modify the processor design by adding custom multiplier with a range of verifiable multiplier designs. We exploit Symbolic Computer Algebra (SCA) for performing verification of the multipliers and use Binary Decision Diagrams (BDDs) for the other instructions. Although multiplier verification is itself a challenging task, we particularly show that with some constraints on the structure of the multiplier, the verification process can be achieved in polynomial time. We extend the processor design as reported in the earlier work by including custom multipliers that can be verified within reasonable time. We also design the necessary software tools required to automate the entire verification process. The MicroRV32 RISC-V processor is used as a case study to evaluate the proposed verification methodology. Experimental results show that formal verification can indeed be performed within polynomial bounds for some of the processor units.