diff options
| author | Benedikt Tutzer <e1225461@student.tuwien.ac.at> | 2019-04-30 13:22:33 +0200 | 
|---|---|---|
| committer | Benedikt Tutzer <e1225461@student.tuwien.ac.at> | 2019-04-30 13:22:33 +0200 | 
| commit | dc06e3a28bdb902d9b95d5d4ff2f163ee010aff4 (patch) | |
| tree | 8d6a4b7ebcf96a2fe5b5bdb21b821555a3a3b994 /tests | |
| parent | 124a284487ce4c7b58f2377f04123e15e83e478d (diff) | |
| parent | 314ff1e4ca00ef8024bbb0d2f031efd78b01f9a1 (diff) | |
| download | yosys-dc06e3a28bdb902d9b95d5d4ff2f163ee010aff4.tar.gz yosys-dc06e3a28bdb902d9b95d5d4ff2f163ee010aff4.tar.bz2 yosys-dc06e3a28bdb902d9b95d5d4ff2f163ee010aff4.zip | |
Merge branch 'master' of https://github.com/YosysHQ/yosys into feature/python_bindings
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/aiger/.gitignore | 2 | ||||
| -rw-r--r-- | tests/sat/counters-repeat.v | 38 | ||||
| -rw-r--r-- | tests/sat/counters-repeat.ys | 10 | ||||
| -rw-r--r-- | tests/simple/retime.v | 6 | ||||
| -rwxr-xr-x | tests/tools/autotest.sh | 4 | ||||
| -rw-r--r-- | tests/various/hierarchy.sh | 1 | ||||
| -rw-r--r-- | tests/various/pmux2shiftx.v | 34 | ||||
| -rw-r--r-- | tests/various/pmux2shiftx.ys | 28 | 
8 files changed, 121 insertions, 2 deletions
| diff --git a/tests/aiger/.gitignore b/tests/aiger/.gitignore new file mode 100644 index 000000000..073f46157 --- /dev/null +++ b/tests/aiger/.gitignore @@ -0,0 +1,2 @@ +*.log +*.out diff --git a/tests/sat/counters-repeat.v b/tests/sat/counters-repeat.v new file mode 100644 index 000000000..2ea45499a --- /dev/null +++ b/tests/sat/counters-repeat.v @@ -0,0 +1,38 @@ +// coverage for repeat loops outside of constant functions + +module counter1(clk, rst, ping); +	input clk, rst; +	output ping; +	reg [31:0] count; + +	always @(posedge clk) begin +		if (rst) +			count <= 0; +		else +			count <= count + 1; +	end + +	assign ping = &count; +endmodule + +module counter2(clk, rst, ping); +	input clk, rst; +	output ping; +	reg [31:0] count; + +	integer i; +	reg carry; + +	always @(posedge clk) begin +		carry = 1; +		i = 0; +		repeat (32) begin +			count[i] <= !rst & (count[i] ^ carry); +			carry = count[i] & carry; +			i = i+1; +		end +	end + +	assign ping = &count; +endmodule + diff --git a/tests/sat/counters-repeat.ys b/tests/sat/counters-repeat.ys new file mode 100644 index 000000000..b3dcfe08a --- /dev/null +++ b/tests/sat/counters-repeat.ys @@ -0,0 +1,10 @@ + +read_verilog counters-repeat.v +proc; opt + +expose -shared counter1 counter2 +miter -equiv -make_assert -make_outputs counter1 counter2 miter + +cd miter; flatten; opt +sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs + diff --git a/tests/simple/retime.v b/tests/simple/retime.v new file mode 100644 index 000000000..30b6087dc --- /dev/null +++ b/tests/simple/retime.v @@ -0,0 +1,6 @@ +module retime_test(input clk, input [7:0] a, output z); +    reg [7:0] ff = 8'hF5; +    always @(posedge clk) +        ff <= {ff[6:0], ^a}; +    assign z = ff[7]; +endmodule diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh index f3dac504e..bb9c3bfb5 100755 --- a/tests/tools/autotest.sh +++ b/tests/tools/autotest.sh @@ -7,7 +7,7 @@ use_modelsim=false  verbose=false  keeprunning=false  makejmode=false -frontend="verilog" +frontend="verilog -noblackbox"  backend_opts="-noattr -noexpr -siminit"  autotb_opts=""  include_opts="" @@ -137,7 +137,7 @@ do  			egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext}  		else  			"$toolsdir"/../../yosys -f "$frontend $include_opts" -b "verilog" -o ${bn}_ref.v ../${fn} -			frontend="verilog" +			frontend="verilog -noblackbox"  		fi  		if [ ! -f ../${bn}_tb.v ]; then diff --git a/tests/various/hierarchy.sh b/tests/various/hierarchy.sh index d33a247be..9dbd1c89f 100644 --- a/tests/various/hierarchy.sh +++ b/tests/various/hierarchy.sh @@ -53,6 +53,7 @@ echo -n "  no explicit top - "      module noTop(a, y);        input a;        output [31:0] y; +      assign y = a;      endmodule    EOV    hierarchy -auto-top diff --git a/tests/various/pmux2shiftx.v b/tests/various/pmux2shiftx.v new file mode 100644 index 000000000..fec84187b --- /dev/null +++ b/tests/various/pmux2shiftx.v @@ -0,0 +1,34 @@ +module pmux2shiftx_test ( +	input [2:0] S1, +	input [5:0] S2, +	input [1:0] S3, +	input [9:0] A, B, C, D, D, E, F, G, H, +	input [9:0] I, J, K, L, M, N, O, P, Q, +	output reg [9:0] X +); +	always @* begin +		case (S1) +			3'd 0: X = A; +			3'd 1: X = B; +			3'd 2: X = C; +			3'd 3: X = D; +			3'd 4: X = E; +			3'd 5: X = F; +			3'd 6: X = G; +			3'd 7: X = H; +		endcase +		case (S2) +			6'd 45: X = I; +			6'd 47: X = J; +			6'd 49: X = K; +			6'd 55: X = L; +			6'd 57: X = M; +			6'd 59: X = N; +		endcase +		case (S3) +			2'd 1: X = O; +			2'd 2: X = P; +			2'd 3: X = Q; +		endcase +	end +endmodule diff --git a/tests/various/pmux2shiftx.ys b/tests/various/pmux2shiftx.ys new file mode 100644 index 000000000..deb134083 --- /dev/null +++ b/tests/various/pmux2shiftx.ys @@ -0,0 +1,28 @@ +read_verilog pmux2shiftx.v +prep +design -save gold + +pmux2shiftx -min_density 70 + +opt + +stat +# show -width +select -assert-count 1 t:$sub +select -assert-count 1 t:$mux +select -assert-count 1 t:$shift +select -assert-count 3 t:$shiftx + +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports miter + +design -load gold +stat + +design -load gate +stat | 
