Vericert can be used to translate a subset of C into Verilog.