ymherklotz / vericert

A formally verified high-level synthesis tool based on CompCert and written in Coq.
https://vericert.ymhg.org
GNU General Public License v3.0
86 stars 5 forks source link

ill-formed initializer issue #14

Open nanoeng opened 2 years ago

nanoeng commented 2 years ago

Howdy,

I'm trying to generate run a 4 tap FIR filter and I'm getting the error message shown below

Would appreciate any help to find a potential solution.

command: ./bin/vericert fir_4tap.c -o fir_4tap.o

error message fir_4tap.c:5:31: syntax error after '{' and before '}'. Ill-formed initializer. At this point, an optional designation, followed with an initializer, is expected. Fatal error; compilation aborted. 1 error detected.

code The FIR filter I'm trying to implement is described below (example taken from the Parallel Programming for FPGAs' book)

define NUM_TAPS 4

void fir ( int input, int output, int taps [NUM_TAPS] ) { static int delay_line [NUM_TAPS] = {}; int result = 0; for ( int i = NUM_TAPS -1 ; i > 0 ; i--) { delay_line[i] = delay_line[i - 1]; } delay_line[0] = input; for ( int i = 0 ; i < NUM_TAPS ; i ++ ) { result += delay_line[i] taps[i]; } *output = result; }

ymherklotz commented 2 years ago

Hi, the first issue you mention is actually a parsing issue with CompCert, it just doesn't allow empty initialiser lists. Instead the following will actually parse and compile with CompCert:

#define NUM_TAPS 4
void fir ( int input, int *output, int taps [NUM_TAPS] ) {

    static int delay_line [NUM_TAPS] = {0};

    int result = 0;

    for ( int i = NUM_TAPS -1 ; i > 0 ; i--) {
        delay_line[i] = delay_line[i - 1];
    }

    delay_line[0] = input;

    for ( int i = 0 ; i < NUM_TAPS ; i ++ ) {
        result += delay_line[i] * taps[i];
    }

    *output = result;
}

Finally though, unfortunavely Vericert doesn't support a large subset of C yet, so the designs that you can compile at the moment don't really look like typical HLS designs as you have written here. The below function will at least compile and kind of do what you want:

#define NUM_TAPS 4
int main ( int input ) {

    int taps [NUM_TAPS] = {1, 2, 3, 4};

    int delay_line [NUM_TAPS] = {0};

    int result = 0;

    for ( int i = NUM_TAPS -1 ; i > 0 ; i--) {
        delay_line[i] = delay_line[i - 1];
    }

    delay_line[0] = input;

    for ( int i = 0 ; i < NUM_TAPS ; i ++ ) {
        result += delay_line[i] * taps[i];
    }

    return result;
}

In general though, the things that you are using which are not supported in Vericert but used all the time in HLS are (which actually incidentally all have to do with the simplistic memory handling in Vericert:

Thanks for trying out Vericert though! I'm happy you managed to compile it in the first place. I hope this helps, and let me know if you have any thoughts.

ymherklotz commented 2 years ago

But I will admit, without static the second design I posted does not implement an FIR filter.

nanoeng commented 2 years ago

Thanks a lot for the detailed reply!