| #!/bin/bash |
| |
| exec 2>&1 |
| set -ex |
| |
| export SCRIPT=/home/dan/work/rnd/opencores/tools/mcy/scripts/create_mutated.sh |
| # create_mutated.sh -c |
| . ${SCRIPT} -c |
| ## create yosys script with instructions how to export the mutated design |
| # { |
| # # read synthesized design |
| # echo "read_ilang ../../database/design.il" |
| # while read -r idx mut; do |
| # # add mutation to the design, to be enabled by value ${idx} on 8-bit input `mutsel` added to the module |
| # echo "mutate -ctrl mutsel 8 ${idx} ${mut#* }" |
| # done < 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_eq.sv . |
| ln -s ../../test_fm.sby . |
| ln -s ../../faxil_slave.v . |
| ln -s ../../easyaxil_tb.sv . |
| # sed -e '1,$s/easyaxil/goldenaxil/' < ../../easyaxil.v > goldenaxil.v |
| |
| sby -f test_fm.sby bmc |
| |
| ## obtain result |
| gawk "{ print 1, \$1; }" test_fm_bmc/status >> output.txt |
| |
| exit 0 |
