search

ghdl / ghdl-yosys-plugin

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

testsuite: Add formal tests #57

Closed tmeissner closed 4 years ago

tmeissner commented 4 years ago

This PR adds infrastructure and tests for functionality, not only synthesizability. Tests are done with formal verification using SymbiYosys.

For this reason ghdl/synth:formal is used instead of ghdl/synth:beta. As it is a superset of ghdl/synth:beta, it can be used for all tests, not only the formal ones.

There are some changes to the test infrastructure to support that, together with moving the existing tests under a new sub directory issues/. Together with the new sub directory formal/ it should be easier for a later integration of ghdlsynth-beta in GHDL.

@1138-4EB: Thanks for contributing to this PR (Travis & Docker).

@tgingold: Is this PR okay, or should I combine the various commits? Other problems that could prevent merging?

tgingold commented 4 years ago

That's great! Thanks!

eine commented 4 years ago

For this reason ghdl/synth:formal is used instead of ghdl/synth:beta. As it is a superset of ghdl/synth:beta, it can be used for all tests, not only the formal ones.

This is a note to myself: now that ghdl/synth:formal is built with travis.sh from this repo, we can remove the corresponding Dockerfile and job from repo ghdl/docker.

@tgingold, @tmeissner, while I was having a look and fixing the Travis/Docker setup, I found that failures produced by z3 not being found would not make the testsuite fail! Hence, we need to take care, because having all green doesn't mean that formal verification is being executed successfully. This is not the case for synthesis. Therefore, I think that there might be some difference between how yosys' and symbiyosys' return codes. See, for example, https://travis-ci.com/1138-4EB/ghdlsynth-beta/builds/130602844#L1442. Unfortunately I couldn't find how to fix it.

tmeissner commented 4 years ago

@1138-4EB If an PSL assertion was proved as wrong, the return value shows that an error occurred. Do you mean errors before the verification process during synthesis? Ah, okay, for example, when z3 isn't found.