From 360f1b03a3ada03344832add89e29ee2ec12ff06 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 9 Jul 2025 10:04:37 +1200 Subject: [PATCH] tests/intertask: Use bash script Somewhat hacky use of the automatic task collection splitting tasks into separate make targets. --- tests/intertask/cancelledby.sby | 16 +++++++++------- tests/intertask/cancelledby.sh | 23 +++++++++++++++++++++++ 2 files changed, 32 insertions(+), 7 deletions(-) create mode 100644 tests/intertask/cancelledby.sh diff --git a/tests/intertask/cancelledby.sby b/tests/intertask/cancelledby.sby index 6163874..e5771ab 100644 --- a/tests/intertask/cancelledby.sby +++ b/tests/intertask/cancelledby.sby @@ -10,28 +10,30 @@ c: a [options] mode bmc -depth 10000 -expect fail,cancelled +depth 20 +a: expect pass,cancelled +b: expect fail,cancelled +c: expect fail,cancelled [engines] btor btormc [script] -a: read -define MAX=9600 -b: read -define MAX=1267 -c: read -define MAX=7200 +a: read -define MAX=32 +b: read -define MAX=12 +c: read -define MAX=3 read -formal demo.sv prep -top demo [file demo.sv] module demo ( input clk, - output reg [31:0] counter + output reg [5:0] counter ); initial counter = 0; always @(posedge clk) begin - if (counter[31] == 1'b1) + if (counter == 15) counter <= 0; else counter <= counter + 1; diff --git a/tests/intertask/cancelledby.sh b/tests/intertask/cancelledby.sh new file mode 100644 index 0000000..9eb6b41 --- /dev/null +++ b/tests/intertask/cancelledby.sh @@ -0,0 +1,23 @@ +#!/bin/bash +set -e + +if [[ $TASK == a ]]; then + # different process, no cancellations + python3 $SBY_MAIN --prefix $WORKDIR -f $SBY_FILE a + python3 $SBY_MAIN --prefix $WORKDIR -f $SBY_FILE b + python3 $SBY_MAIN --prefix $WORKDIR -f $SBY_FILE c + test -e ${WORKDIR}_a/PASS -a -e ${WORKDIR}_b/FAIL -a -e ${WORKDIR}_c/FAIL +elif [[ $TASK == b ]]; then + # same process, a cancels c cancels b + # use statusdb so that the different taskloops from using --sequential doesn't matter + python3 $SBY_MAIN --prefix $WORKDIR -f $SBY_FILE --statusreset || true + python3 $SBY_MAIN --prefix $WORKDIR -f $SBY_FILE a c b --sequential --statuscancels + test -e ${WORKDIR}_a/PASS -a -e ${WORKDIR}_b/CANCELLED -a -e ${WORKDIR}_c/CANCELLED +else + # different process, b cancels a, c completes before a + python3 $SBY_MAIN --prefix $WORKDIR -f $SBY_FILE --statusreset || true + python3 $SBY_MAIN --prefix $WORKDIR -f $SBY_FILE b --statuscancels + python3 $SBY_MAIN --prefix $WORKDIR -f $SBY_FILE c --statuscancels + python3 $SBY_MAIN --prefix $WORKDIR -f $SBY_FILE a --statuscancels + echo test -e ${WORKDIR}_a/CANCELLED -a -e ${WORKDIR}_b/FAIL -a -e ${WORKDIR}_c/FAIL +fi