From bdaa8844be64818cab4bd8e77e91bb7af0bfcf98 Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Sun, 17 Jan 2021 10:18:00 +0000 Subject: deploy: 91ef287ac751a674fab3ecf089101fa2b6062a97 --- docs/index.html | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'docs/index.html') diff --git a/docs/index.html b/docs/index.html index 1e4364f..0e096bc 100644 --- a/docs/index.html +++ b/docs/index.html @@ -1,7 +1,7 @@ Docs | Vericert -
+ The design shown in Figure 1 shows how Vericert leverages an existing verified C compiler called CompCert to perform this translation.">Docs | Vericert +
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 called CompCert to perform this translation.

\ No newline at end of file +

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 called CompCert to perform this translation.

\ No newline at end of file -- cgit