Using Vericert

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