summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-03-17 01:56:00 +0100
committerClifford Wolf <clifford@clifford.at>2014-03-17 01:56:00 +0100
commita67cd2d4a284cb945af6d477cc215cef7bdd22a8 (patch)
tree2be5f13ffe5ecdec4fc365bba955ccd83258254c /tests
parentacda74c12cd39ae1a17d15f472728b49ad584e91 (diff)
Progress in Verific bindings
Diffstat (limited to 'tests')
-rw-r--r--tests/simple/forgen01.v3
-rw-r--r--tests/simple/mem_arst.v2
-rwxr-xr-xtests/tools/autotest.sh10
3 files changed, 13 insertions, 2 deletions
diff --git a/tests/simple/forgen01.v b/tests/simple/forgen01.v
index 70ee7e66..8b7aa279 100644
--- a/tests/simple/forgen01.v
+++ b/tests/simple/forgen01.v
@@ -1,3 +1,6 @@
+
+// VERIFIC-SKIP
+
module uut_forgen01(a, y);
input [4:0] a;
diff --git a/tests/simple/mem_arst.v b/tests/simple/mem_arst.v
index 4022f57c..9bd38fcb 100644
--- a/tests/simple/mem_arst.v
+++ b/tests/simple/mem_arst.v
@@ -10,7 +10,7 @@ module MyMem #(
output [DataWidth-1:0] Data_o,
input WR_i);
- reg Data_o;
+ reg [DataWidth-1:0] Data_o;
localparam Size = 2**AddrWidth;
diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index fafd044d..d459f988 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -82,7 +82,7 @@ do
[[ "$bn" == *_tb ]] && continue
echo -n "Test: $bn "
- rm -f ${bn}.{err,log}
+ rm -f ${bn}.{err,log,sikp}
mkdir -p ${bn}.out
rm -rf ${bn}.out/*
@@ -111,6 +111,11 @@ do
test_count=$(( test_count + 1 ))
}
+ if [ "$frontend" = "verific" -o "$frontend" = "verific_gates" ] && grep -q VERIFIC-SKIP $fn; then
+ touch ../${bn}.skip
+ return
+ fi
+
if [ -n "$scriptfiles" ]; then
test_passes $fn $scriptfiles
elif [ -n "$scriptopt" ]; then
@@ -137,6 +142,9 @@ do
if [ -f ${bn}.log ]; then
mv ${bn}.err ${bn}.log
echo "-> ok"
+ elif [ -f ${bn}.skip ]; then
+ mv ${bn}.err ${bn}.skip
+ echo "-> skip"
else echo "-> ERROR!"; $keeprunning || exit 1; fi
done