Using Vericert
Vericert can be used to translate a subset of C into Verilog. As a simple example, consider the
following C file (main.c
):
void matrix_multiply(int first[2][2], int second[2][2], int multiply[2][2]) {
int sum = 0;
for (int c = 0; c < 2; c++) {
for (int d = 0; d < 2; d++) {
for (int k = 0; k < 2; k++) {
sum = sum + first[c][k]*second[k][d];
}
multiply[c][d] = sum;
sum = 0;
}
}
}
int main() {
int f[2][2] = {{1, 2}, {3, 4}};
int s[2][2] = {{5, 6}, {7, 8}};
int m[2][2] = {{0, 0}, {0, 0}};
matrix_multiply(f, s, m);
return m[1][1];
}
It can be compiled using the following command, assuming that vericert is somewhere on the path.
vericert main.c -o main.v
The Verilog file contains a top-level test-bench, which can be given to any Verilog simulator to simulate the hardware, which should give the same result as executing the C code. Using Icarus Verilog as an example:
iverilog -o main_v main.v
When executing, it should therefore print the following:
$ ./main_v
finished: 50
This gives the same result as executing the C in the following way:
$ gcc -o main_c main.c
$ ./main_c
$ echo $?
50