From 83aaa860b691697d59b83fadac2c4dad51972387 Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Mon, 20 Sep 2021 09:02:50 +0000 Subject: deploy: d9f8dee1a294ee087f56c6e54b16ad3b0bf8d895 --- docs/index.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'docs/index.html') diff --git a/docs/index.html b/docs/index.html index 6b5a5be..03748e7 100644 --- a/docs/index.html +++ b/docs/index.html @@ -6,5 +6,5 @@ Docs

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).

Figure 1: Current design of Vericert, where HTL is an intermediate language representing a finite state machine with data-path (FSMD) and Verilog is the target language.

Figure 1: Current design of Vericert, where HTL is an intermediate language representing a finite state machine with data-path (FSMD) and Verilog is the target language.

The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler +application-specific integrated circuit (ASIC).

Figure 1: Current design of Vericert, where HTL is an intermediate language representing a finite state machine with data-path (FSMD) and Verilog is the target language.

Figure 1: Current design of Vericert, where HTL is an intermediate language representing a finite state machine with data-path (FSMD) and Verilog is the target language.

The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation.

\ No newline at end of file -- cgit