aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/aiger/.gitignore3
-rwxr-xr-xtests/aiger/run-test.sh10
-rw-r--r--tests/simple/arrays02.sv16
-rw-r--r--tests/simple/defvalue.sv22
-rw-r--r--tests/simple/generate.v11
-rwxr-xr-xtests/tools/autotest.sh29
-rw-r--r--tests/various/.gitignore3
-rw-r--r--tests/various/signext.ys33
8 files changed, 106 insertions, 21 deletions
diff --git a/tests/aiger/.gitignore b/tests/aiger/.gitignore
index 073f46157..9a26bb8f4 100644
--- a/tests/aiger/.gitignore
+++ b/tests/aiger/.gitignore
@@ -1,2 +1 @@
-*.log
-*.out
+/*_ref.v
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh
index f52eb4ac1..5246c1b48 100755
--- a/tests/aiger/run-test.sh
+++ b/tests/aiger/run-test.sh
@@ -10,8 +10,9 @@ for aag in *.aag; do
# Since ABC cannot read *.aag, read the *.aig instead
# (which would have been created by the reference aig2aig utility,
# available from http://fmv.jku.at/aiger/)
- ../../yosys-abc -c "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
- ../../yosys -p "
+ echo "Checking $aag."
+ ../../yosys-abc -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
+ ../../yosys -qp "
read_verilog ${aag%.*}_ref.v
prep
design -stash gold
@@ -26,8 +27,9 @@ sat -verify -prove-asserts -show-ports -seq 16 miter
done
for aig in *.aig; do
- ../../yosys-abc -c "read -c $aig; write ${aig%.*}_ref.v"
- ../../yosys -p "
+ echo "Checking $aig."
+ ../../yosys-abc -q "read -c $aig; write ${aig%.*}_ref.v"
+ ../../yosys -qp "
read_verilog ${aig%.*}_ref.v
prep
design -stash gold
diff --git a/tests/simple/arrays02.sv b/tests/simple/arrays02.sv
new file mode 100644
index 000000000..76c2a7388
--- /dev/null
+++ b/tests/simple/arrays02.sv
@@ -0,0 +1,16 @@
+module uut_arrays02(clock, we, addr, wr_data, rd_data);
+
+input clock, we;
+input [3:0] addr, wr_data;
+output [3:0] rd_data;
+reg [3:0] rd_data;
+
+reg [3:0] memory [16];
+
+always @(posedge clock) begin
+ if (we)
+ memory[addr] <= wr_data;
+ rd_data <= memory[addr];
+end
+
+endmodule
diff --git a/tests/simple/defvalue.sv b/tests/simple/defvalue.sv
new file mode 100644
index 000000000..b0a087ecb
--- /dev/null
+++ b/tests/simple/defvalue.sv
@@ -0,0 +1,22 @@
+module top(input clock, input [3:0] delta, output [3:0] cnt1, cnt2);
+ cnt #(1) foo (.clock, .cnt(cnt1), .delta);
+ cnt #(2) bar (.clock, .cnt(cnt2));
+endmodule
+
+module cnt #(
+ parameter integer initval = 0
+) (
+ input clock,
+ output logic [3:0] cnt = initval,
+`ifdef __ICARUS__
+ input [3:0] delta
+`else
+ input [3:0] delta = 10
+`endif
+);
+`ifdef __ICARUS__
+ assign (weak0, weak1) delta = 10;
+`endif
+ always @(posedge clock)
+ cnt <= cnt + delta;
+endmodule
diff --git a/tests/simple/generate.v b/tests/simple/generate.v
index 3c55682cb..0e353ad9b 100644
--- a/tests/simple/generate.v
+++ b/tests/simple/generate.v
@@ -148,3 +148,14 @@ generate
endgenerate
assign out = steps[WIDTH].outer[0].val;
endmodule
+
+// ------------------------------------------
+
+module gen_test6(output [3:0] o);
+generate
+ genvar i;
+ for (i = 3; i >= 0; i = i-1) begin
+ assign o[i] = 1'b0;
+ end
+endgenerate
+endmodule
diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index 23964a751..96d9cdda9 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -89,8 +89,7 @@ done
compile_and_run() {
exe="$1"; output="$2"; shift 2
- ext=${1##*.}
- if [ "$ext" == "sv" ]; then
+ if [ "${2##*.}" == "sv" ]; then
language_gen="-g2012"
else
language_gen="-g2005"
@@ -142,23 +141,25 @@ do
cd ${bn}.out
fn=$(basename $fn)
bn=$(basename $bn)
+ refext=v
rm -f ${bn}_ref.fir
if [[ "$ext" == "v" ]]; then
egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext}
elif [[ "$ext" == "aig" ]] || [[ "$ext" == "aag" ]]; then
- "$toolsdir"/../../yosys-abc -c "read_aiger ../${fn}; write ${bn}_ref.v"
+ "$toolsdir"/../../yosys-abc -c "read_aiger ../${fn}; write ${bn}_ref.${refext}"
else
- cp ../${fn} ${bn}_ref.${ext}
+ refext=$ext
+ cp ../${fn} ${bn}_ref.${refext}
fi
if [ ! -f ../${bn}_tb.v ]; then
- "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.v
+ "$toolsdir"/../../yosys -f "$frontend $include_opts" -b "test_autotb $autotb_opts" -o ${bn}_tb.v ${bn}_ref.${refext}
else
cp ../${bn}_tb.v ${bn}_tb.v
fi
if $genvcd; then sed -i 's,// \$dump,$dump,g' ${bn}_tb.v; fi
- compile_and_run ${bn}_tb_ref ${bn}_out_ref ${bn}_tb.v ${bn}_ref.v $libs \
+ compile_and_run ${bn}_tb_ref ${bn}_out_ref ${bn}_tb.v ${bn}_ref.${refext} $libs \
"$toolsdir"/../../techlibs/common/simlib.v \
"$toolsdir"/../../techlibs/common/simcells.v
if $genvcd; then mv testbench.vcd ${bn}_ref.vcd; fi
@@ -175,25 +176,25 @@ do
test_count=$(( test_count + 1 ))
}
- if [ "$frontend" = "verific" -o "$frontend" = "verific_gates" ] && grep -q VERIFIC-SKIP ${bn}_ref.v; then
+ if [ "$frontend" = "verific" -o "$frontend" = "verific_gates" ] && grep -q VERIFIC-SKIP ${bn}_ref.${refext}; then
touch ../${bn}.skip
return
fi
if [ -n "$scriptfiles" ]; then
- test_passes -f "$frontend $include_opts" ${bn}_ref.v $scriptfiles
+ test_passes -f "$frontend $include_opts" ${bn}_ref.${refext} $scriptfiles
elif [ -n "$scriptopt" ]; then
- test_passes -f "$frontend $include_opts" -p "$scriptopt" ${bn}_ref.v
+ test_passes -f "$frontend $include_opts" -p "$scriptopt" ${bn}_ref.${refext}
elif [ "$frontend" = "verific" ]; then
- test_passes -p "verific -vlog2k ${bn}_ref.v; verific -import -all; opt; memory;;"
+ test_passes -p "verific -vlog2k ${bn}_ref.${refext}; verific -import -all; opt; memory;;"
elif [ "$frontend" = "verific_gates" ]; then
- test_passes -p "verific -vlog2k ${bn}_ref.v; verific -import -gates -all; opt; memory;;"
+ test_passes -p "verific -vlog2k ${bn}_ref.${refext}; verific -import -gates -all; opt; memory;;"
else
- test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.v
- test_passes -f "$frontend $include_opts" -p "hierarchy; synth -run coarse; techmap; opt; abc -dff" ${bn}_ref.v
+ test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.${refext}
+ test_passes -f "$frontend $include_opts" -p "hierarchy; synth -run coarse; techmap; opt; abc -dff" ${bn}_ref.${refext}
if [ -n "$firrtl2verilog" ]; then
if test -z "$xfirrtl" || ! grep "$fn" "$xfirrtl" ; then
- "$toolsdir"/../../yosys -b "firrtl" -o ${bn}_ref.fir -f "$frontend $include_opts" -p "prep -nordff; proc; opt; memory; opt; fsm; opt -full -fine; pmuxtree" ${bn}_ref.v
+ "$toolsdir"/../../yosys -b "firrtl" -o ${bn}_ref.fir -f "$frontend $include_opts" -p "prep -nordff; proc; opt; memory; opt; fsm; opt -full -fine; pmuxtree" ${bn}_ref.${refext}
$firrtl2verilog -i ${bn}_ref.fir -o ${bn}_ref.fir.v
test_passes -f "$frontend $include_opts" -p "hierarchy; proc; opt; memory; opt; fsm; opt -full -fine" ${bn}_ref.fir.v
fi
diff --git a/tests/various/.gitignore b/tests/various/.gitignore
index 397b4a762..7b3e8c68e 100644
--- a/tests/various/.gitignore
+++ b/tests/various/.gitignore
@@ -1 +1,2 @@
-*.log
+/*.log
+/*.out
diff --git a/tests/various/signext.ys b/tests/various/signext.ys
new file mode 100644
index 000000000..0c8d671e7
--- /dev/null
+++ b/tests/various/signext.ys
@@ -0,0 +1,33 @@
+
+read_verilog -formal <<EOT
+module gate(input clk, output [32:0] o, p, q, r, s, t, u);
+assign o = 'bx;
+assign p = 1'bx;
+assign q = 'bz;
+assign r = 1'bz;
+assign s = 1'b0;
+assign t = 'b1;
+assign u = -'sb1;
+endmodule
+EOT
+
+proc
+
+## Equivalence checking
+
+read_verilog -formal <<EOT
+module gold(input clk, output [32:0] o, p, q, r, s, t, u);
+assign o = {33{1'bx}};
+assign p = {{32{1'b0}}, 1'bx};
+assign q = {33{1'bz}};
+assign r = {{32{1'b0}}, 1'bz};
+assign s = {33{1'b0}};
+assign t = {{32{1'b0}}, 1'b1};
+assign u = {33{1'b1}};
+endmodule
+EOT
+
+proc
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports -enable_undef miter