3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-08-14 08:55:27 +00:00

tests/intertask: Use bash script

Somewhat hacky use of the automatic task collection splitting tasks into separate make targets.
This commit is contained in:
Krystine Sherwin 2025-07-09 10:04:37 +12:00
parent 67212a20e5
commit 360f1b03a3
No known key found for this signature in database
2 changed files with 32 additions and 7 deletions

View file

@ -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;

View file

@ -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