equivalence checking between C and Verilog codes.

[cs17...@smail.iitm.ac.in]

HI,

Is it possible to use hw-cbmc to do equivalence checking between a C and a Verilog code snippet that do the same job.

For eg - a multiplication function that is implemented in C as well as Verilog.

Is it possible to prove that the two codes are equivalent or otherwise. 

As of now Im trying to analyze C code by CBMC, Verilog code through hw-cbmc and then comparing both results.

Is there a better way and can I be pointed to the right examples.

Thanks

Ram