Algorithmic datapath designs are typically modelled at a high level in C/C++ and can be verified at early stages before the corresponding RTL design is ready. The criticality for the equivalence verification of datapath designs (RTL) with their reference high-level C/C++ models, is well accepted. Simulation-based approaches like DPI or scoreboarding suffer from challenges of achieving verification completeness. The means of verifying this equivalence is shifting from simulation to formal gradually, thanks to new solver capabilities available in commercial formal tools and the exhaustive nature of formal. However complex image processing algorithms often run into the challenge of compiling i.e. building the formal model from C++ of in reasonable time. Also, we often struggle to achieve proof convergence on the equivalence check targets, even if we manage to compile the C/C++ models. While formal methods can be potentially effective, the right methodology is required to overcome these challenges and scale to larger and complex designs. In this paper, we propose several generic techniques that have helped us to generate formal models for FFT and Decompression units in a couple of minutes and converge on the properties which was impossible to achieve out of the box. In this process, we uncovered bugs that traditional verification methods failed to detect. All these techniques are reusable. This paper presents details of these techniques by taking an FFT and a Decompression algorithm as an example.