tests/aiger/run-test.sh

   1 #!/bin/bash
   2
   3 set -e
   4
   5 # NB: *.aag and *.aig must contain a symbol table naming the primary
   6 #     inputs and outputs, otherwise ABC and Yosys will name them
   7 #     arbitrarily (and inconsistently with each other).
   8
   9 for aag in *.aag; do
  10     # Since ABC cannot read *.aag, read the *.aig instead
  11     # (which would have been created by the reference aig2aig utility,
  12     #  available from http://fmv.jku.at/aiger/)
  13     ../../yosys-abc -c "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
  14     ../../yosys -p "
  15 read_verilog ${aag%.*}_ref.v
  16 prep
  17 design -stash gold
  18 read_aiger -clk_name clock $aag
  19 prep
  20 design -stash gate
  21 design -import gold -as gold
  22 design -import gate -as gate
  23 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  24 sat -verify -prove-asserts -show-ports -seq 16 miter
  25 "
  26 done
  27
  28 for aig in *.aig; do
  29     ../../yosys-abc -c "read -c $aig; write ${aig%.*}_ref.v"
  30     ../../yosys -p "
  31 read_verilog ${aig%.*}_ref.v
  32 prep
  33 design -stash gold
  34 read_aiger -clk_name clock $aig
  35 prep
  36 design -stash gate
  37 design -import gold -as gold
  38 design -import gate -as gate
  39 miter -equiv -flatten -make_assert -make_outputs gold gate miter
  40 sat -verify -prove-asserts -show-ports -seq 16 miter
  41 "
  42 done