tests/sva/runtest.sh

   1 #!/bin/bash
   2
   3 set -ex
   4
   5 prefix=${1%.ok}
   6 prefix=${prefix%.sv}
   7 prefix=${prefix%.vhd}
   8 test -f $prefix.sv -o -f $prefix.vhd
   9
  10 generate_sby() {
  11         cat <<- EOT
  12                 [options]
  13                 mode bmc
  14                 depth 10
  15                 expect $1
  16
  17                 [engines]
  18                 smtbmc yices
  19
  20                 [script]
  21         EOT
  22
  23         if [ -f $prefix.sv ]; then
  24                 if [ "$1" = "fail" ]; then
  25                         echo "verific -sv ${prefix}_fail.sv"
  26                 else
  27                         echo "verific -sv $prefix.sv"
  28                 fi
  29         fi
  30
  31         if [ -f $prefix.vhd ]; then
  32                 echo "verific -vhdl $prefix.vhd"
  33         fi
  34
  35         cat <<- EOT
  36                 verific -import -extnets -all top
  37                 prep -top top
  38                 chformal -early -assume
  39
  40                 [files]
  41         EOT
  42
  43         if [ -f $prefix.sv ]; then
  44                 echo "$prefix.sv"
  45         fi
  46
  47         if [ -f $prefix.vhd ]; then
  48                 echo "$prefix.vhd"
  49         fi
  50
  51         if [ "$1" = "fail" ]; then
  52                 cat <<- EOT
  53
  54                         [file ${prefix}_fail.sv]
  55                         \`define FAIL
  56                         \`include "$prefix.sv"
  57                 EOT
  58         fi
  59 }
  60
  61 if [ -f $prefix.sv ]; then
  62         generate_sby pass > ${prefix}_pass.sby
  63         generate_sby fail > ${prefix}_fail.sby
  64         sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby
  65         sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby
  66 else
  67         generate_sby pass > ${prefix}.sby
  68         sby --yosys $PWD/../../yosys -f ${prefix}.sby
  69 fi
  70
  71 touch $prefix.ok
  72