search

ghdl / ghdl-yosys-plugin

VHDL synthesis (based on ghdl)
GNU General Public License v3.0
304 stars 31 forks source link

Handle Id_Asr #55

Closed tmeissner closed 5 years ago

tmeissner commented 5 years ago

This PR adds handling of Id_Asr for supporting shift_right(signed, nat) of numeric_std.

I've tested the handling of the shift functions. The tests will follow later, as they rely on SymbiYosys to formally verify the results. Don't know how to integrate such tests here at the moment, maybe @1138-4EB could help.

eine commented 5 years ago

Currently, Symbiyosys is absolutely ignored in this repo. However, building a docker image in travis.sh would be as simple as adding a line to build https://github.com/ghdl/docker/blob/master/dockerfiles/synth_formal.

Then, we can just change the image in

https://github.com/tgingold/ghdlsynth-beta/blob/14b5cbdad8da4e0957f02dd94e3ff94d49772f18/travis.sh#L72-L75

to use ghdl/synth:formal, instead of ghdl:synth:beta.

Hence, you can add your tests as additional subdirs in https://github.com/tgingold/ghdlsynth-beta/tree/master/testsuite, or you can add a formal subdir and put a each formal test in a separate subdir in it.

Also, at some point these tests might be merged into https://github.com/ghdl/ghdl/tree/master/testsuite. Foreseeing that scenario, it might be desirable to have a specific formal subdir.

tgingold commented 5 years ago

Thanks!

tmeissner commented 5 years ago

@1138-4EB Honestly, I don't really see through all these Travis stuff :-/

I agree to have a new folder formal, as synth in GHDL for example. However, with that, all the other tests have to be in subfolders also. If not, the path to the utils.sh script don't works for the formal tests. Maybe, all the other tests should move in a folder called synth.

I have a branch at https://github.com/tmeissner/ghdlsynth-beta/tree/formal_tests which contains the formal folder with the new tests and some changes to the test script. Maybe, you can have a look.

eine commented 5 years ago

@1138-4EB Honestly, I don't really see through all these Travis stuff :-/

In this repo only, it is quite simple. All we do is execute https://github.com/tgingold/ghdlsynth-beta/blob/master/travis.sh. Anyway, don't worry; i'll take care.

I agree to have a new folder formal, as synth in GHDL for example. However, with that, all the other tests have to be in subfolders also. If not, the path to the utils.sh script don't works for the formal tests.

You don't need to worry about utils.sh. That's sourced by testsuite/testsuite.sh. This will further execute testsuite/*/testsuite.sh, but not testsuite/**/testsuite.sh:

Note that the first four cases are kind of individual tests and the last three are multitests. So, your testsuite/formal/testsuite.sh would look like:

#!/bin/sh

cd $(dirname $0)

. ../testenv.sh

for d in */; do
    if [ -f $d/testsuite.sh ]; then
        travis_start "test" "$d" "$ANSI_CYAN"
        cd $d
        if ./testsuite.sh; then
            printf "${ANSI_GREEN}OK$ANSI_NOCOLOR\n"
        else
            printf "${ANSI_RED}FAILED!$ANSI_NOCOLOR\n"
            exit 1
        fi
        cd ..
        travis_finish "test"
    else
        printf "${ANSI_YELLOW}Skip $d (no testsuite.sh)$ANSI_NOCOLOR\n"
    fi
    clean
done

This is very much the same approach as in https://github.com/ghdl/ghdl/tree/master/testsuite. Note that each subdir contains a testsuite.sh, and each subsubdir another one.

Maybe, all the other tests should move in a folder called synth.

I think this is a good idea, independently of the comments above.

I have a branch at tmeissner/ghdlsynth-beta@formal_tests which contains the formal folder with the new tests and some changes to the test script. Maybe, you can have a look.

I will. Expect a comment or PR in the following hours.