Skip to content

Y
yosys-tests
Commit 8b04cc85 by Clifford Wolf
Options

Add SVA consrep, gotorep, nonconsrep tests 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
parent c32816fe
Showing with 268 additions and 1 deletions
verific/sva/Makefile
TESTS := firstmatch intersect seq_and seq_or triggered until until_trig within
TESTS := consrep firstmatch gotorep intersect nonconsrep seq_and seq_or triggered until until_trig within
all: $(addsuffix .status,$(TESTS))
grep -H . *.status | sed 's,.status:,\t,; s,PASS,pass,;' | expand -t20
......
verific/sva/consrep.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 throughout ((C ##1 D) [*3])) ##1 !B);
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 throughout ((C ##1 D) [*3])) ##1 !B);
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 throughout ((C ##1 D) [*3])) ##1 !B);
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 throughout ((C ##1 D) [*3])) ##1 !B);
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 throughout ((C ##1 D) [*3])) ##1 !B);
endmodule
verific/sva/gotorep.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 throughout (D [->3])) ##1 C);
endmodule
module pass_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 throughout (D [->3])) ##1 C);
endmodule
module pass_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 throughout (D [->3])) ##1 C);
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 throughout (D [->3])) ##1 C);
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 throughout (D [->3])) ##1 C);
endmodule
verific/sva/nonconsrep.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 throughout (D [=3])) ##1 C);
endmodule
module pass_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 throughout (D [=3])) ##1 C);
endmodule
module pass_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 throughout (D [=3])) ##1 C);
endmodule
module pass_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 throughout (D [=3])) ##1 C);
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 throughout (D [=3])) ##1 C);
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