Behavioral consistency of C and verilog programs using bounded model checking