Traditionally, peak power consumption has been estimated at the module-level and there has been no attempt to check the functional validity of the gate-level estimate through instruction execution. This leads to the overdesign of the processor components that deliver current to the modules. In this work, we present a methodology to estimate the peak dynamic power at the module-level which is functionally valid at the processor-level and thus, avoid the overdesign. We tackle the problem of module-level peak power estimation by building our algorithm using the Reactive Tabu Search technique. We use a bounded model checker for verifying the instruction validity of the module-level peak power estimates at the processor-level. Our algorithm intelligently combines the module-level power estimates with these instruction validity checks and efficiently derives functionally valid peak power estimates. In addition, we automatically derive the sequence of instructions that causes this peak power dissipation for the modules under study. We have evaluated our methodology on modules of the OpenRisc (OR1200) processor and the results demonstrate that our methodology derives the power estimates efficiently.