Hi , need to do a RTL to RTL - logical equivalence checking - which open source tool is best to use ?? ( if it exists !) Thanks in advance

Yosys does have support for adding equivalence cells and generating miter circuits from them. Then you can use its formal verification functionality. Here's an example: https://stackoverflow.com/questions/47745223/reset-behavior-with-miter-equivalence-checking