tests/aiger/run-test.sh

   1 #!/bin/bash
   2
   3 set -e
   4
   5 OPTIND=1
   6 abcprog="../../yosys-abc"    # default to built-in version of abc
   7 while getopts "A:" opt
   8 do
   9     case "$opt" in
  10         A) abcprog="$OPTARG" ;;
  11     esac
  12 done
  13 shift "$((OPTIND-1))"
  14
  15 # NB: *.aag and *.aig must contain a symbol table naming the primary
  16 #     inputs and outputs, otherwise ABC and Yosys will name them
  17 #     arbitrarily (and inconsistently with each other).
  18
  19 for aag in *.aag; do
  20     # Since ABC cannot read *.aag, read the *.aig instead
  21     # (which would have been created by the reference aig2aig utility,
  22     #  available from http://fmv.jku.at/aiger/)
  23     echo "Checking $aag."
  24     $abcprog -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
  25     ../../yosys -qp "
  26 read_verilog ${aag%.*}_ref.v
  27 prep
  28 design -stash gold
  29 read_aiger -clk_name clock $aag
  30 prep
  31 design -stash gate
  32 design -import gold -as gold
  33 design -import gate -as gate
  34 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  35 sat -verify -prove-asserts -show-ports -seq 16 miter
  36 " -l ${aag}.log
  37 done
  38
  39 for aig in *.aig; do
  40     echo "Checking $aig."
  41     $abcprog -q "read -c $aig; write ${aig%.*}_ref.v"
  42     ../../yosys -qp "
  43 read_verilog ${aig%.*}_ref.v
  44 prep
  45 design -stash gold
  46 read_aiger -clk_name clock $aig
  47 prep
  48 design -stash gate
  49 design -import gold -as gold
  50 design -import gate -as gate
  51 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  52 sat -verify -prove-asserts -show-ports -seq 16 miter
  53 " -l ${aig}.log
  54 done
  55
  56 for y in *.ys; do
  57     echo "Running $y."
  58     ../../yosys -ql ${y%.*}.log $y
  59 done