Skip to content

Y
yosys-tests
Commit 98f4dedc by Clifford Wolf
Options

Some fixes related to SVA consecutive repetition 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
parent 8b04cc85
Showing with 133 additions and 16 deletions
verific/sva/Makefile
TESTS := consrep firstmatch gotorep intersect nonconsrep seq_and seq_or triggered until until_trig within
TESTS := consrep firstmatch gotorep intersect nonconsrep seq_and seq_or triggered until until_trig within repzero
all: $(addsuffix .status,$(TESTS))
grep -H . *.status | sed 's,.status:,\t,; s,PASS,pass,;' | expand -t20
......
verific/sva/firstmatch.sv
......@@ -46,7 +46,7 @@ module fail_01 (input clock);
assert property (@(posedge clock) (A ##1 B [*] ##1 C |=> D));
endmodule
module fail_02 (input clock);
module pass_02 (input clock);
wire A, B, C, D;
sequencer #(
......@@ -60,7 +60,21 @@ module fail_02 (input clock);
assert property (@(posedge clock) (first_match(A ##1 B [*] ##1 C) |=> D));
endmodule
module pass_03 (input clock);
module fail_03 (input clock);
wire A, B, C, D;
sequencer #(
// 01234567890123456789012345678901
.trace_a("_-___-__________________________"),
.trace_b("__-------------_________________"),
.trace_c("______-____-___-________________"),
.trace_d("_______-________________________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (first_match(A ##1 B [+] ##1 C) |=> D));
endmodule
module pass_04 (input clock);
wire A, B, C, D;
sequencer #(
......@@ -74,7 +88,7 @@ module pass_03 (input clock);
assert property (@(posedge clock) (first_match(A ##1 B [*] ##1 C) |=> D));
endmodule
module pass_04 (input clock);
module pass_05 (input clock);
wire A, B, C, D;
sequencer #(
......@@ -87,3 +101,17 @@ module pass_04 (input clock);
assert property (@(posedge clock) (first_match(A ##1 B [*] ##1 C) |=> D));
endmodule
module fail_06 (input clock);
wire A, B, C, D;
sequencer #(
// 01234567890123456789012345678901
.trace_a("_-____-_________________________"),
.trace_b("__-------------_________________"),
.trace_c("______-____-___-________________"),
.trace_d("_______-________________________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (first_match(A ##1 B [*] ##1 C) |=> D));
endmodule
verific/sva/intersect.sv
......@@ -29,7 +29,7 @@ module pass_00 (input clock);
.trace_d("_____________-__-_______________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> ((B ##1 !B [*] ##1 B) intersect (C [*] ##1 D)) ##1 B ##1 C ##1 D));
assert property (@(posedge clock) (A |=> ((B ##1 !B [*] ##1 B) intersect (C [+] ##1 D)) ##1 B ##1 C ##1 D));
endmodule
module fail_01 (input clock);
......@@ -43,7 +43,7 @@ module fail_01 (input clock);
.trace_d("_____________-__-_______________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> ((B ##1 !B [*] ##1 B) intersect (C [*] ##1 D)) ##1 B ##1 C ##1 D));
assert property (@(posedge clock) (A |=> ((B ##1 !B [*] ##1 B) intersect (C [+] ##1 D)) ##1 B ##1 C ##1 D));
endmodule
module fail_02 (input clock);
......@@ -57,7 +57,7 @@ module fail_02 (input clock);
.trace_d("_____________-__-_______________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> ((B ##1 !B [*] ##1 B) intersect (C [*] ##1 D)) ##1 B ##1 C ##1 D));
assert property (@(posedge clock) (A |=> ((B ##1 !B [*] ##1 B) intersect (C [+] ##1 D)) ##1 B ##1 C ##1 D));
endmodule
module fail_03 (input clock);
......@@ -71,7 +71,7 @@ module fail_03 (input clock);
.trace_d("_____________-___-______________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> ((B ##1 !B [*] ##1 B) intersect (C [*] ##1 D)) ##1 B ##1 C ##1 D));
assert property (@(posedge clock) (A |=> ((B ##1 !B [*] ##1 B) intersect (C [+] ##1 D)) ##1 B ##1 C ##1 D));
endmodule
module fail_04 (input clock);
......@@ -85,5 +85,5 @@ module fail_04 (input clock);
.trace_d("____________-___-_______________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> ((B ##1 !B [*] ##1 B) intersect (C [*] ##1 D)) ##1 B ##1 C ##1 D));
assert property (@(posedge clock) (A |=> ((B ##1 !B [*] ##1 B) intersect (C [+] ##1 D)) ##1 B ##1 C ##1 D));
endmodule
verific/sva/repzero.sv 0 → 100644
module sequencer #(
// 01234567890123456789012345678901
parameter [32*8-1:0] trace_a = "________________________________",
parameter [32*8-1:0] trace_b = "________________________________",
parameter [32*8-1:0] trace_c = "________________________________",
parameter [32*8-1:0] trace_d = "________________________________"
) (
input clock,
output A, B, C, D
);
integer t = 0;
always @(posedge clock) t <= t + (t < 31);
assign A = trace_a[8*(31-t) +: 8] == "-";
assign B = trace_b[8*(31-t) +: 8] == "-";
assign C = trace_c[8*(31-t) +: 8] == "-";
assign D = trace_d[8*(31-t) +: 8] == "-";
endmodule
module pass_00 (input clock);
wire A, B, C, D;
sequencer #(
// 01234567890123456789012345678901
.trace_a("_-__________-_____-_____________"),
.trace_b("__-__________-_____-_____-______"),
.trace_c("___------_____-_________________"),
.trace_d("_________-_____-____-________-__")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) A |=> B ##1 C [*] ##1 D);
endmodule
module fail_01 (input clock);
wire A, B, C, D;
sequencer #(
// 01234567890123456789012345678901
.trace_a("_-__________-_____-_____________"),
.trace_b("__-__________-_____-_____-______"),
.trace_c("___--_---_____-_________________"),
.trace_d("_________-_____-____-________-__")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) A |=> B ##1 C [*] ##1 D);
endmodule
module fail_02 (input clock);
wire A, B, C, D;
sequencer #(
// 01234567890123456789012345678901
.trace_a("_-__________-_____-_____________"),
.trace_b("__-__________-_____-_____-______"),
.trace_c("___------_______________________"),
.trace_d("_________-_____-____-________-__")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) A |=> B ##1 C [*] ##1 D);
endmodule
module fail_03 (input clock);
wire A, B, C, D;
sequencer #(
// 01234567890123456789012345678901
.trace_a("_-__________-_____-_____________"),
.trace_b("__-__________-_____-_____-______"),
.trace_c("___------_____-_________________"),
.trace_d("_________-_____-___-_________-__")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) A |=> B ##1 C [*] ##1 D);
endmodule
module fail_04 (input clock);
wire A, B, C, D;
sequencer #(
// 01234567890123456789012345678901
.trace_a("_-__________-_____-_____-_______"),
.trace_b("__-__________-_____-_____-______"),
.trace_c("___------_____-_________________"),
.trace_d("_________-_____-____-________-__")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) A |=> B ##1 C [*] ##1 D);
endmodule
verific/sva/within.sv
......@@ -29,7 +29,7 @@ module pass_00 (input clock);
.trace_d("______-______-__________________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> (B [*3] within (C [*])) ##1 D));
assert property (@(posedge clock) (A |=> (B [*3] within (C [+])) ##1 D));
endmodule
module pass_01 (input clock);
......@@ -43,7 +43,7 @@ module pass_01 (input clock);
.trace_d("________-_______________________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> (B [*3] within (C [*])) ##1 D));
assert property (@(posedge clock) (A |=> (B [*3] within (C [+])) ##1 D));
endmodule
module fail_02 (input clock);
......@@ -57,7 +57,7 @@ module fail_02 (input clock);
.trace_d("_______-________________________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> (B [*3] within (C [*])) ##1 D));
assert property (@(posedge clock) (A |=> (B [*3] within (C [+])) ##1 D));
endmodule
module fail_03 (input clock);
......@@ -71,7 +71,7 @@ module fail_03 (input clock);
.trace_d("_______-________________________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> (B [*3] within (C [*])) ##1 D));
assert property (@(posedge clock) (A |=> (B [*3] within (C [+])) ##1 D));
endmodule
module fail_04 (input clock);
......@@ -85,7 +85,7 @@ module fail_04 (input clock);
.trace_d("_______-________________________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> (B [*3] within (C [*])) ##1 D));
assert property (@(posedge clock) (A |=> (B [*3] within (C [+])) ##1 D));
endmodule
module pass_05 (input clock);
......@@ -99,7 +99,7 @@ module pass_05 (input clock);
.trace_d("_______-________________________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> (B [*3] within (C [*])) ##1 D));
assert property (@(posedge clock) (A |=> (B [*3] within (C [+])) ##1 D));
endmodule
module pass_06 (input clock);
......@@ -113,5 +113,5 @@ module pass_06 (input clock);
.trace_d("_______-________________________")
) uut (clock, A, B, C, D);
assert property (@(posedge clock) (A |=> (B [*3] within (C [*])) ##1 D));
assert property (@(posedge clock) (A |=> (B [*3] within (C [+])) ##1 D));
endmodule
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment