.travis.yml

# TODO: Extend this to add job(s) for simulations, can be run in parallel with risc-v formal.

dist: trusty
sudo: false
language: generic

cache:
  directories:
    -  /home/travis/build/$TRAVIS_PULL_REQUEST_SLUG/formal/env
    -  /home/travis/build/$TRAVIS_REPO_SLUG/formal/env

before_install:
install:
  # If env is not provided by the cache and marked passed, remove any cached env results and build it.
  - ( cd formal && if [[ ! -e env/PASSED ]]; then rm -rf env/* && ./make_env.sh; fi )
  # Record the commit ID of the latest yosys.
  - git ls-remote --heads https://github.com/cliffordwolf/yosys.git refs/heads/master > yosys_latest_commit_id.txt && sed -i 's/\s.*//' yosys_latest_commit_id.txt
  # Record the commit ID of the latest SymbiYosys.
  - git ls-remote --heads https://github.com/cliffordwolf/SymbiYosys.git refs/heads/master > SymbiYosys_latest_commit_id.txt && sed -i 's/\s.*//' SymbiYosys_latest_commit_id.txt

before_script:
  - cd formal
  - if ("$TRAVIS_PULL_REQUEST"); then export BUILD_PATH=$TRAVIS_PULL_REQUEST_SLUG; else export BUILD_PATH=$TRAVIS_REPO_SLUG; fi

# TODO : riscv-formal for 6 stage implementation
jobs :
  include :
    - stage : "Check all 3 configs with risc-v formal" # Run riscv-formal for WARP-V.
      name : "1 Stage - riscv-formal"
      script: 
      -  sed -i "/-stage/c\   m4_define([\'M4_STANDARD_CONFIG\'], [\'1-stage\'])" /home/travis/build/$BUILD_PATH/formal/warp-v_formal.tlv
      -  sed -i "/insn   /c\insn            20" /home/travis/build/$BUILD_PATH/formal/checks.cfg
      -  PATH=/home/travis/build/$BUILD_PATH/formal/env/bin:$PATH bash -c 'make verif';
    - script: 
      -  sed -i "/-stage/c\   m4_define([\'M4_STANDARD_CONFIG\'], [\'4-stage\'])" /home/travis/build/$BUILD_PATH/formal/warp-v_formal.tlv
      -  sed -i "/insn   /c\insn            29" /home/travis/build/$BUILD_PATH/formal/checks.cfg
      -  PATH=/home/travis/build/$BUILD_PATH/formal/env/bin:$PATH bash -c 'make verif';
      name : "4 Stage - riscv-formal"
      # the structure for the YAML format is non-standard in some way, but Travis interprets it correctly
      # with both the scripts being run parallel under same stage (in Travis terminology)

after_success:
after_failure:
  # Upload files for debug.
  - echo "Uploading up to 4 failure traces for debug" && for FILE in `ls /home/travis/build/$BUILD_PATH/formal/checks/*/FAIL | head -n 4`; do curl --upload-file `echo $FILE | sed s/FAIL$//`engine_0/trace.vcd https://transfer.sh/`echo $FILE | sed 's/^.*\/\([^\/]*\)\/FAIL$/\1/'`_trace.vcd && echo; done
after_script:
  # Report a message if we didn't use the latest commit of yosys.
  - if cmp -s yosys_latest_commit_id.txt env/yosys_commit_id.txt; then echo '******** Using the following cached yosys (https://github.com/cliffordwolf/yosys.git) commit ID which is not the latest. Consider clearing Travis cache. **********' && cat env/yosys_commit_id.txt && echo '**********'; fi
  # Report a message if we didn't use the latest commit of SymbiYosys.
  - if cmp -s SymbiYosys_latest_commit_id.txt env/SymbiYosys_commit_id.txt; then echo '******** Using the following cached SymbiYosys (https://github.com/cliffordwolf/SymbiYosys) commit ID which is not the latest. Consider clearing Travis cache. **********' && cat env/SymbiYosys_commit_id.txt && echo '**********'; fi