Vericert translates C code into a hardware description language called Verilog, which can then be synthesised into hardware, to be placed onto a field-programmable gate array (FPGA) or application-specific integrated circuit (ASIC).
The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation.