| #!/bin/bash |
| |
| exec 2>&1 |
| set -ex |
| |
| export SCRIPT=/home/dan/work/rnd/opencores/tools/mcy/scripts/create_mutated.sh |
| # create_mutated.sh |
| . ${SCRIPT} |
| |
| ## create yosys script with instructions how to export the mutated design |
| # { |
| # # read synthesized design |
| # echo "read_ilang ../../database/design.il" |
| # # apply mutation |
| # # First line is numbered one, two, etc. |
| # # This cust off the '1' in the beginning, keeps the rest of the |
| # # mutate command |
| # cut -f2- -d' ' input.txt |
| # # export design to RTLIL |
| # echo "write_ilang mutated.il" |
| # echo "write_verilog mutated.v" |
| #} > mutate.ys |
| |
| ## run the above script to create mutated.il |
| yosys -ql mutate.log mutate.ys |
| |
| ## run formal property check |
| ln -s ../../test_fm.sby . |
| ln -s ../../faxil_slave.v . |
| ln -s ../../easyprops.sv . |
| |
| sby -f test_fm.sby prf |
| |
| ## obtain result |
| gawk "{ print 1, \$1; }" test_fm_prf/status | sed -e "s/UNKNOWN/FAIL/" >> output.txt |
| |
| exit 0 |
