From 5033b51947a6ef02cb785b5622e993335efa750a Mon Sep 17 00:00:00 2001 From: Ruben Undheim Date: Thu, 30 Aug 2018 20:46:20 +0200 Subject: New upstream version 0.7+20180830git0b7a184 --- tests/sat/sizebits.sv | 32 ++++++++++++++++++ tests/sat/sizebits.ys | 2 ++ tests/simple/arraycells.v | 2 +- tests/simple/graphtest.v | 2 +- tests/simple/hierdefparam.v | 23 +++++++++++++ tests/simple/specify.v | 31 +++++++++++++++++ tests/sva/.gitignore | 7 ++++ tests/sva/Makefile | 13 ++++++++ tests/sva/basic00.sv | 12 +++++++ tests/sva/basic01.sv | 16 +++++++++ tests/sva/basic02.sv | 20 +++++++++++ tests/sva/basic03.sv | 12 +++++++ tests/sva/basic04.sv | 10 ++++++ tests/sva/basic04.vhd | 26 +++++++++++++++ tests/sva/basic05.sv | 19 +++++++++++ tests/sva/basic05.vhd | 26 +++++++++++++++ tests/sva/counter.sv | 30 +++++++++++++++++ tests/sva/runtest.sh | 72 +++++++++++++++++++++++++++++++++++++++ tests/sva/sva_not.sv | 34 +++++++++++++++++++ tests/sva/sva_range.sv | 19 +++++++++++ tests/sva/sva_throughout.sv | 19 +++++++++++ tests/tools/autotest.sh | 4 +-- tests/unit/Makefile | 35 +++++++++++++++++++ tests/unit/kernel/logTest.cc | 14 ++++++++ tests/unit/kernel/rtlilTest.cc | 14 ++++++++ tests/various/reg_wire_error.sv | 74 +++++++++++++++++++++++++++++++++++++++++ tests/various/reg_wire_error.ys | 1 + 27 files changed, 565 insertions(+), 4 deletions(-) create mode 100644 tests/sat/sizebits.sv create mode 100644 tests/sat/sizebits.ys create mode 100644 tests/simple/hierdefparam.v create mode 100644 tests/simple/specify.v create mode 100644 tests/sva/.gitignore create mode 100644 tests/sva/Makefile create mode 100644 tests/sva/basic00.sv create mode 100644 tests/sva/basic01.sv create mode 100644 tests/sva/basic02.sv create mode 100644 tests/sva/basic03.sv create mode 100644 tests/sva/basic04.sv create mode 100644 tests/sva/basic04.vhd create mode 100644 tests/sva/basic05.sv create mode 100644 tests/sva/basic05.vhd create mode 100644 tests/sva/counter.sv create mode 100644 tests/sva/runtest.sh create mode 100644 tests/sva/sva_not.sv create mode 100644 tests/sva/sva_range.sv create mode 100644 tests/sva/sva_throughout.sv create mode 100644 tests/unit/Makefile create mode 100644 tests/unit/kernel/logTest.cc create mode 100644 tests/unit/kernel/rtlilTest.cc create mode 100644 tests/various/reg_wire_error.sv create mode 100644 tests/various/reg_wire_error.ys (limited to 'tests') diff --git a/tests/sat/sizebits.sv b/tests/sat/sizebits.sv new file mode 100644 index 00000000..d7ce2326 --- /dev/null +++ b/tests/sat/sizebits.sv @@ -0,0 +1,32 @@ +module functions01; + +wire [5:2]x; +wire [3:0]y[2:7]; +wire [3:0]z[7:2][2:9]; + +//wire [$size(x)-1:0]x_size; +//wire [$size({x, x})-1:0]xx_size; +//wire [$size(y)-1:0]y_size; +//wire [$size(z)-1:0]z_size; + +assert property ($size(x) == 4); +assert property ($size({3{x}}) == 3*4); +assert property ($size(y) == 6); +assert property ($size(y, 1) == 6); +assert property ($size(y, (1+1)) == 4); + +assert property ($size(z) == 6); +assert property ($size(z, 1) == 6); +assert property ($size(z, 2) == 8); +assert property ($size(z, 3) == 4); +// This should trigger an error if enabled (it does). +//assert property ($size(z, 4) == 4); + +//wire [$bits(x)-1:0]x_bits; +//wire [$bits({x, x})-1:0]xx_bits; + +assert property ($bits(x) == 4); +assert property ($bits(y) == 4*6); +assert property ($bits(z) == 4*6*8); + +endmodule diff --git a/tests/sat/sizebits.ys b/tests/sat/sizebits.ys new file mode 100644 index 00000000..689227a4 --- /dev/null +++ b/tests/sat/sizebits.ys @@ -0,0 +1,2 @@ +read_verilog -sv sizebits.sv +prep; sat -verify -prove-asserts diff --git a/tests/simple/arraycells.v b/tests/simple/arraycells.v index 704ca3fd..fd85a119 100644 --- a/tests/simple/arraycells.v +++ b/tests/simple/arraycells.v @@ -2,7 +2,7 @@ module array_test001(a, b, c, y); input a; input [31:0] b, c; - input [31:0] y; + output [31:0] y; aoi12 p [31:0] (a, b, c, y); endmodule diff --git a/tests/simple/graphtest.v b/tests/simple/graphtest.v index 74788dbb..9b16b61c 100644 --- a/tests/simple/graphtest.v +++ b/tests/simple/graphtest.v @@ -25,7 +25,7 @@ assign Z[7:4] = {1'b0, B[2:0]}; // Concat of CV and PI connect to PO always @* begin if (A == 4'b1111) begin // All-Const at port (eq) X = B; - end + end else begin X = 4'b0000; // All-Const at port (mux) end diff --git a/tests/simple/hierdefparam.v b/tests/simple/hierdefparam.v new file mode 100644 index 00000000..ff92c38b --- /dev/null +++ b/tests/simple/hierdefparam.v @@ -0,0 +1,23 @@ +module hierdefparam_top(input [7:0] A, output [7:0] Y); + generate begin:foo + hierdefparam_a mod_a(.A(A), .Y(Y)); + end endgenerate + defparam foo.mod_a.bar[0].mod_b.addvalue = 42; + defparam foo.mod_a.bar[1].mod_b.addvalue = 43; +endmodule + +module hierdefparam_a(input [7:0] A, output [7:0] Y); + genvar i; + generate + for (i = 0; i < 2; i=i+1) begin:bar + wire [7:0] a, y; + hierdefparam_b mod_b(.A(a), .Y(y)); + end + endgenerate + assign bar[0].a = A, bar[1].a = bar[0].y, Y = bar[1].y; +endmodule + +module hierdefparam_b(input [7:0] A, output [7:0] Y); + parameter [7:0] addvalue = 44; + assign Y = A + addvalue; +endmodule diff --git a/tests/simple/specify.v b/tests/simple/specify.v new file mode 100644 index 00000000..f19418d9 --- /dev/null +++ b/tests/simple/specify.v @@ -0,0 +1,31 @@ +module test_specify; + +specparam a=1; + +specify +endspecify + +specify +(A => B) = ( 1 ) ; +(A- => B) = ( 1,2 ) ; +(A+ => B) = ( 1,2,3 ) ; +(A => B) = ( + 1.1, 2, 3, + 4, 5.5, 6.6 +) ; +(A => B) = ( + 1.1, 2, 3, + 4, 5.5, 6.6 , + 7.7, 8.8, 9, + 10.1, 11, 12 +) ; +specparam b=1; +specparam [1:2] asasa=1; +endspecify + +specify +specparam c=1:2:3; +endspecify + +endmodule + diff --git a/tests/sva/.gitignore b/tests/sva/.gitignore new file mode 100644 index 00000000..cc254049 --- /dev/null +++ b/tests/sva/.gitignore @@ -0,0 +1,7 @@ +/*_pass.sby +/*_fail.sby +/*_pass +/*_fail +/*.ok +/vhdlpsl[0-9][0-9] +/vhdlpsl[0-9][0-9].sby diff --git a/tests/sva/Makefile b/tests/sva/Makefile new file mode 100644 index 00000000..1b217f74 --- /dev/null +++ b/tests/sva/Makefile @@ -0,0 +1,13 @@ + +TESTS = $(sort $(basename $(wildcard *.sv)) $(basename $(wildcard *.vhd))) + +all: $(addsuffix .ok,$(TESTS)) + +%.ok: + bash runtest.sh $@ + +clean: + rm -rf $(addsuffix .ok,$(TESTS)) $(addsuffix .sby,$(TESTS)) $(TESTS) + rm -rf $(addsuffix _pass.sby,$(TESTS)) $(addsuffix _pass,$(TESTS)) + rm -rf $(addsuffix _fail.sby,$(TESTS)) $(addsuffix _fail,$(TESTS)) + diff --git a/tests/sva/basic00.sv b/tests/sva/basic00.sv new file mode 100644 index 00000000..30c37f5f --- /dev/null +++ b/tests/sva/basic00.sv @@ -0,0 +1,12 @@ +module top (input clk, reset, antecedent, output reg consequent); + always @(posedge clk) + consequent <= reset ? 0 : antecedent; + +`ifdef FAIL + test_assert: assert property ( @(posedge clk) disable iff (reset) antecedent |-> consequent ) + else $error("Failed with consequent = ", $sampled(consequent)); +`else + test_assert: assert property ( @(posedge clk) disable iff (reset) antecedent |=> consequent ) + else $error("Failed with consequent = ", $sampled(consequent)); +`endif +endmodule diff --git a/tests/sva/basic01.sv b/tests/sva/basic01.sv new file mode 100644 index 00000000..74ab9343 --- /dev/null +++ b/tests/sva/basic01.sv @@ -0,0 +1,16 @@ +module top (input logic clock, ctrl); + logic read = 0, write = 0, ready = 0; + + always @(posedge clock) begin + read <= !ctrl; + write <= ctrl; + ready <= write; + end + + a_rw: assert property ( @(posedge clock) !(read && write) ); +`ifdef FAIL + a_wr: assert property ( @(posedge clock) write |-> ready ); +`else + a_wr: assert property ( @(posedge clock) write |=> ready ); +`endif +endmodule diff --git a/tests/sva/basic02.sv b/tests/sva/basic02.sv new file mode 100644 index 00000000..b34f3aff --- /dev/null +++ b/tests/sva/basic02.sv @@ -0,0 +1,20 @@ +module top (input logic clock, ctrl); + logic read = 0, write = 0, ready = 0; + + always @(posedge clock) begin + read <= !ctrl; + write <= ctrl; + ready <= write; + end +endmodule + +module top_properties (input logic clock, read, write, ready); + a_rw: assert property ( @(posedge clock) !(read && write) ); +`ifdef FAIL + a_wr: assert property ( @(posedge clock) write |-> ready ); +`else + a_wr: assert property ( @(posedge clock) write |=> ready ); +`endif +endmodule + +bind top top_properties properties_inst (.*); diff --git a/tests/sva/basic03.sv b/tests/sva/basic03.sv new file mode 100644 index 00000000..8018de4c --- /dev/null +++ b/tests/sva/basic03.sv @@ -0,0 +1,12 @@ +module top (input logic clk, input logic selA, selB, QA, QB, output logic Q); + always @(posedge clk) begin + if (selA) Q <= QA; + if (selB) Q <= QB; + end + + check_selA: assert property ( @(posedge clk) selA |=> Q == $past(QA) ); + check_selB: assert property ( @(posedge clk) selB |=> Q == $past(QB) ); +`ifndef FAIL + assume_not_11: assume property ( @(posedge clk) !(selA & selB) ); +`endif +endmodule diff --git a/tests/sva/basic04.sv b/tests/sva/basic04.sv new file mode 100644 index 00000000..bc46be9f --- /dev/null +++ b/tests/sva/basic04.sv @@ -0,0 +1,10 @@ +module top_properties (input logic clock, read, write, ready); + a_rw: assert property ( @(posedge clock) !(read && write) ); +`ifdef FAIL + a_wr: assert property ( @(posedge clock) write |-> ready ); +`else + a_wr: assert property ( @(posedge clock) write |=> ready ); +`endif +endmodule + +bind top top_properties properties_inst (.*); diff --git a/tests/sva/basic04.vhd b/tests/sva/basic04.vhd new file mode 100644 index 00000000..f2ec305e --- /dev/null +++ b/tests/sva/basic04.vhd @@ -0,0 +1,26 @@ +library ieee; +use ieee.std_logic_1164.all; + +entity top is + port ( + clock : in std_logic; + ctrl : in std_logic; + x : out std_logic + ); +end entity; + +architecture rtl of top is + signal read : std_logic := '0'; + signal write : std_logic := '0'; + signal ready : std_logic := '0'; +begin + process (clock) begin + if (rising_edge(clock)) then + read <= not ctrl; + write <= ctrl; + ready <= write; + end if; + end process; + + x <= read xor write xor ready; +end architecture; diff --git a/tests/sva/basic05.sv b/tests/sva/basic05.sv new file mode 100644 index 00000000..816ee1da --- /dev/null +++ b/tests/sva/basic05.sv @@ -0,0 +1,19 @@ +module top (input logic clock, ctrl); + logic read, write, ready; + + demo uut ( + .clock(clock), + .ctrl(ctrl) + ); + + assign read = uut.read; + assign write = uut.write; + assign ready = uut.ready; + + a_rw: assert property ( @(posedge clock) !(read && write) ); +`ifdef FAIL + a_wr: assert property ( @(posedge clock) write |-> ready ); +`else + a_wr: assert property ( @(posedge clock) write |=> ready ); +`endif +endmodule diff --git a/tests/sva/basic05.vhd b/tests/sva/basic05.vhd new file mode 100644 index 00000000..8d42f71e --- /dev/null +++ b/tests/sva/basic05.vhd @@ -0,0 +1,26 @@ +library ieee; +use ieee.std_logic_1164.all; + +entity demo is + port ( + clock : in std_logic; + ctrl : in std_logic; + x : out std_logic + ); +end entity; + +architecture rtl of demo is + signal read : std_logic := '0'; + signal write : std_logic := '0'; + signal ready : std_logic := '0'; +begin + process (clock) begin + if (rising_edge(clock)) then + read <= not ctrl; + write <= ctrl; + ready <= write; + end if; + end process; + + x <= read xor write xor ready; +end architecture; diff --git a/tests/sva/counter.sv b/tests/sva/counter.sv new file mode 100644 index 00000000..4f949115 --- /dev/null +++ b/tests/sva/counter.sv @@ -0,0 +1,30 @@ +module top (input clk, reset, up, down, output reg [7:0] cnt); + always @(posedge clk) begin + if (reset) + cnt <= 0; + else if (up) + cnt <= cnt + 1; + else if (down) + cnt <= cnt - 1; + end + + default clocking @(posedge clk); endclocking + default disable iff (reset); + + assert property (up |=> cnt == $past(cnt) + 8'd 1); + assert property (up [*2] |=> cnt == $past(cnt, 2) + 8'd 2); + assert property (up ##1 up |=> cnt == $past(cnt, 2) + 8'd 2); + +`ifndef FAIL + assume property (down |-> !up); +`endif + assert property (up ##1 down |=> cnt == $past(cnt, 2)); + assert property (down |=> cnt == $past(cnt) - 8'd 1); + + property down_n(n); + down [*n] |=> cnt == $past(cnt, n) - n; + endproperty + + assert property (down_n(8'd 3)); + assert property (down_n(8'd 5)); +endmodule diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh new file mode 100644 index 00000000..1b65ca9c --- /dev/null +++ b/tests/sva/runtest.sh @@ -0,0 +1,72 @@ +#!/bin/bash + +set -ex + +prefix=${1%.ok} +prefix=${prefix%.sv} +prefix=${prefix%.vhd} +test -f $prefix.sv -o -f $prefix.vhd + +generate_sby() { + cat <<- EOT + [options] + mode bmc + depth 10 + expect $1 + + [engines] + smtbmc yices + + [script] + EOT + + if [ -f $prefix.sv ]; then + if [ "$1" = "fail" ]; then + echo "verific -sv ${prefix}_fail.sv" + else + echo "verific -sv $prefix.sv" + fi + fi + + if [ -f $prefix.vhd ]; then + echo "verific -vhdl $prefix.vhd" + fi + + cat <<- EOT + verific -import -extnets -all top + prep -top top + chformal -early -assume + + [files] + EOT + + if [ -f $prefix.sv ]; then + echo "$prefix.sv" + fi + + if [ -f $prefix.vhd ]; then + echo "$prefix.vhd" + fi + + if [ "$1" = "fail" ]; then + cat <<- EOT + + [file ${prefix}_fail.sv] + \`define FAIL + \`include "$prefix.sv" + EOT + fi +} + +if [ -f $prefix.sv ]; then + generate_sby pass > ${prefix}_pass.sby + generate_sby fail > ${prefix}_fail.sby + sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby + sby --yosys $PWD/../../yosys -f ${prefix}_fail.sby +else + generate_sby pass > ${prefix}.sby + sby --yosys $PWD/../../yosys -f ${prefix}.sby +fi + +touch $prefix.ok + diff --git a/tests/sva/sva_not.sv b/tests/sva/sva_not.sv new file mode 100644 index 00000000..d81a4865 --- /dev/null +++ b/tests/sva/sva_not.sv @@ -0,0 +1,34 @@ +module top ( + input clk, + input reset, + input ping, + input [1:0] cfg, + output reg pong +); + reg [2:0] cnt; + localparam integer maxdelay = 8; + + always @(posedge clk) begin + if (reset) begin + cnt <= 0; + pong <= 0; + end else begin + cnt <= cnt - |cnt; + pong <= cnt == 1; + if (ping) cnt <= 4 + cfg; + end + end + + assert property ( + @(posedge clk) + disable iff (reset) + not (ping ##1 !pong [*maxdelay]) + ); + +`ifndef FAIL + assume property ( + @(posedge clk) + not (cnt && ping) + ); +`endif +endmodule diff --git a/tests/sva/sva_range.sv b/tests/sva/sva_range.sv new file mode 100644 index 00000000..d1569fc8 --- /dev/null +++ b/tests/sva/sva_range.sv @@ -0,0 +1,19 @@ +module top ( + input clk, + input a, b, c, d +); + default clocking @(posedge clk); endclocking + + assert property ( + a ##[*] b |=> c until d + ); + +`ifndef FAIL + assume property ( + b |=> ##5 d + ); + assume property ( + b || (c && !d) |=> c + ); +`endif +endmodule diff --git a/tests/sva/sva_throughout.sv b/tests/sva/sva_throughout.sv new file mode 100644 index 00000000..7e036a06 --- /dev/null +++ b/tests/sva/sva_throughout.sv @@ -0,0 +1,19 @@ +module top ( + input clk, + input a, b, c, d +); + default clocking @(posedge clk); endclocking + + assert property ( + a |=> b throughout (c ##1 d) + ); + +`ifndef FAIL + assume property ( + a |=> b && c + ); + assume property ( + b && c |=> b && d + ); +`endif +endmodule diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh index d0b0a89d..d6216244 100755 --- a/tests/tools/autotest.sh +++ b/tests/tools/autotest.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash libs="" genvcd=false @@ -100,7 +100,7 @@ do echo -n "Test: $bn " fi - rm -f ${bn}.{err,log,sikp} + rm -f ${bn}.{err,log,skip} mkdir -p ${bn}.out rm -rf ${bn}.out/* diff --git a/tests/unit/Makefile b/tests/unit/Makefile new file mode 100644 index 00000000..9f1e5c99 --- /dev/null +++ b/tests/unit/Makefile @@ -0,0 +1,35 @@ +GTESTFLAG := -lgtest -lgtest_main +RPATH := -Wl,-rpath +EXTRAFLAGS := -lyosys -pthreads + +OBJTEST := objtest +BINTEST := bintest + +ALLTESTFILE := $(shell find -name '*Test.cc' -printf '%P ') +TESTDIRS := $(sort $(dir $(ALLTESTFILE))) +TESTS := $(addprefix $(BINTEST)/, $(basename $(ALLTESTFILE:%Test.cc=%Test.o))) + +# Prevent make from removing our .o files +.SECONDARY: + +all: prepare $(TESTS) run-tests + +$(BINTEST)/%: $(OBJTEST)/%.o + $(CXX) -L$(ROOTPATH) $(RPATH)=$(ROOTPATH) -o $@ $^ $(LDLIBS) \ + $(GTESTFLAG) $(EXTRAFLAGS) + +$(OBJTEST)/%.o: $(basename $(subst $(OBJTEST),.,%)).cc + $(CXX) -o $@ -c -I$(ROOTPATH) $(CPPFLAGS) $(CXXFLAGS) $^ + +.PHONY: prepare run-tests clean + +run-tests: $(TESTS) + $(subst Test ,Test; ,$^) + +prepare: + mkdir -p $(addprefix $(BINTEST)/,$(TESTDIRS)) + mkdir -p $(addprefix $(OBJTEST)/,$(TESTDIRS)) + +clean: + rm -rf $(OBJTEST) + rm -rf $(BINTEST) diff --git a/tests/unit/kernel/logTest.cc b/tests/unit/kernel/logTest.cc new file mode 100644 index 00000000..62b4f3b9 --- /dev/null +++ b/tests/unit/kernel/logTest.cc @@ -0,0 +1,14 @@ +#include + +#include "kernel/yosys.h" +#include "kernel/log.h" + +YOSYS_NAMESPACE_BEGIN + +TEST(KernelLogTest, logvValidValues) +{ + //TODO: Implement log test + EXPECT_EQ(7, 7); +} + +YOSYS_NAMESPACE_END diff --git a/tests/unit/kernel/rtlilTest.cc b/tests/unit/kernel/rtlilTest.cc new file mode 100644 index 00000000..d9eeed55 --- /dev/null +++ b/tests/unit/kernel/rtlilTest.cc @@ -0,0 +1,14 @@ +#include + +#include "kernel/yosys.h" +#include "kernel/rtlil.h" + +YOSYS_NAMESPACE_BEGIN + +TEST(KernelRtlilTest, getReferenceValid) +{ + //TODO: Implement rtlil test + EXPECT_EQ(33, 33); +} + +YOSYS_NAMESPACE_END diff --git a/tests/various/reg_wire_error.sv b/tests/various/reg_wire_error.sv new file mode 100644 index 00000000..fe5ff3ab --- /dev/null +++ b/tests/various/reg_wire_error.sv @@ -0,0 +1,74 @@ +module sub_mod(input i_in, output o_out); +assign o_out = i_in; +endmodule + +module test(i_clk, i, i_reg, o_reg, o_wire, o_mr, o_mw, o_ml); +input i_clk; +input i; +input i_reg; +output o_reg; +output o_wire; +output o_mr, o_mw, o_ml; + +// Enable this to see how it doesn't fail on yosys although it should +//reg o_wire; +// Enable this instead of the above to see how logic can be mapped to a wire +logic o_wire; +// Enable this to see how it doesn't fail on yosys although it should +//reg i_reg; +// Disable this to see how it doesn't fail on yosys although it should +//reg o_reg; + +logic l_reg; + +// Enable this to tst if logic-turne-reg will catch assignments even if done before it turned into a reg +assign l_reg = !o_reg; +initial o_reg = 1'b0; +always @(posedge i_clk) +begin + o_reg <= !o_reg; + l_reg <= !o_reg; +end + +assign o_wire = !o_reg; +// Uncomment this to see how a logic already turned intoa reg can be freely assigned on yosys +assign l_reg = !o_reg; + +sub_mod sm_inst ( + .i_in(1'b1), + .o_out(o_reg) +); + +wire mw1[0:1]; +wire mw2[0:1]; +wire mw3[0:1]; +reg mr1[0:1]; +reg mr2[0:1]; +reg mr3[0:1]; +logic ml1[0:1]; +logic ml2[0:1]; +logic ml3[0:1]; + +assign o_mw = mw1[i]; +assign o_mr = mr1[i]; +assign o_ml = ml1[i]; + +assign mw1[1] = 1'b1; +//assign mr1[1] = 1'b1; +assign ml1[1] = 1'b1; +always @(posedge i_clk) +begin + mr2[0] = 1'b0; + mw2[0] = 1'b0; + ml2[0] = 1'b0; +end + +always @(posedge i_clk) +begin + mr3[0] <= 1'b0; + mw3[0] <= 1'b0; + ml3[0] <= 1'b0; +end + +endmodule + diff --git a/tests/various/reg_wire_error.ys b/tests/various/reg_wire_error.ys new file mode 100644 index 00000000..b9d03155 --- /dev/null +++ b/tests/various/reg_wire_error.ys @@ -0,0 +1 @@ +read_verilog -sv reg_wire_error.sv -- cgit v1.2.3