Skip to content

Commit

Permalink
Use $anyconst in formal ALU tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@msinger
msinger committed Feb 21, 2021
1 parent b710095 commit 74ac11d
Show file tree
Hide file tree
Showing 37 changed files with 954 additions and 1,098 deletions.
897 changes: 0 additions & 897 deletions tests/alu.svh
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion tests/alu_add.sby.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ bmc: mode bmc
append 10
expect pass
multiclock on
add_bmc: depth 128
add_bmc: depth 20

[engines]
smtbmc
Expand Down
75 changes: 60 additions & 15 deletions tests/alu_add.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,23 +4,68 @@
module testbench(input logic clk);
`include "alu.svh"

localparam SCYC = 2;

logic [7:0] a = $anyconst;
logic [7:0] b = $anyconst;
logic c = $anyconst;

logic [7:0] r;
logic co, ho;

assign { co, r } = a + b + c;
assign ho = !!((a[3:0] + b[3:0] + c) & 'h10);

logic halfcarry, hc_we;
always_ff @(posedge clk) if (hc_we) halfcarry = carry;

always_comb begin
undef_inputs();
hc_we = $anyseq;

line0 = $anyseq;
line0.op = a;
line0.sh = NO_SH;
line0.oe = SH_OE;
line0.la = BUS_LD;

line1 = $anyseq;
line1.la = NO_LD;
line1.op = b;
line1.sh = NO_SH;
line1.oe = SH_OE;
line1.lb = BUS_LD;
line1.r = 0;
line1.s = 0;
line1.v = 0;
line1.ne = 0;
line1.ci = c;
line1.l = 1;
line1.h = 0;

line2 = $anyseq;
line2.la = NO_LD;
line2.lb = NO_LD;
line2.r = 0;
line2.s = 0;
line2.v = 0;
line2.ne = 0;
line2.ci = halfcarry;
line2.l = 0;
line2.h = 1;
line2.oe = RES_OE;

if (cyc == SCYC + 1) hc_we = 1;

if (cyc == SCYC) set_inputs(line0);
if (cyc == SCYC + 1) set_inputs(line1);
if (cyc == SCYC + 2) set_inputs(line2);

/* cyc, opA, opB, C */
test_add( 4, 0, 0, 0);
test_add( 8, 0, 0, 1);
test_add( 12, 255, 255, 1);
test_add( 16, 15, 0, 0);
test_add( 20, 0, 15, 0);
test_add( 24, 15, 0, 1);
test_add( 28, 0, 15, 1);
test_add( 32, 255, 0, 0);
test_add( 36, 255, 0, 1);
test_add( 40, 255, 1, 0);
test_add( 44, 255, 1, 1);
test_add( 48, 254, 1, 0);
test_add( 52, 254, 1, 1);
test_add( 56, 'h77, 'h77, 0);
if (cyc == SCYC + 2) begin
assert(result == r);
assert(carry == co);
assert(halfcarry == ho);
assert(zero == !r);
end
end
endmodule
2 changes: 1 addition & 1 deletion tests/alu_and.sby.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ bmc: mode bmc
append 10
expect pass
multiclock on
and_bmc: depth 72
and_bmc: depth 20

[engines]
smtbmc
Expand Down
62 changes: 54 additions & 8 deletions tests/alu_and.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,16 +4,62 @@
module testbench(input logic clk);
`include "alu.svh"

localparam SCYC = 2;

logic [7:0] a = $anyconst;
logic [7:0] b = $anyconst;

logic [7:0] r;

assign r = a & b;

always_comb begin
undef_inputs();

/* cyc, opA, opB */
test_and( 4, 0, 0);
test_and( 8, 255, 255);
test_and( 12, 255, 0);
test_and( 16, 0, 255);
test_and( 20, 'haa, 'haa);
test_and( 24, 'haa, 'h55);
test_and( 28, 'h21, 'hb9);
line0 = $anyseq;
line0.op = a;
line0.sh = NO_SH;
line0.oe = SH_OE;
line0.la = BUS_LD;

line1 = $anyseq;
line1.la = NO_LD;
line1.op = b;
line1.sh = NO_SH;
line1.oe = SH_OE;
line1.lb = BUS_LD;
line1.r = 0;
line1.s = 1;
line1.v = 0;
line1.ne = 0;
line1.ci = 1;
line1.l = 1;
line1.h = 0;

line2 = $anyseq;
line2.la = NO_LD;
line2.lb = NO_LD;
line2.r = 0;
line2.s = 1;
line2.v = 0;
line2.ne = 0;
line2.ci = 1;
line2.l = 0;
line2.h = 1;
line2.oe = RES_OE;

if (cyc == SCYC) set_inputs(line0);
if (cyc == SCYC + 1) set_inputs(line1);
if (cyc == SCYC + 2) set_inputs(line2);

if (cyc == SCYC + 1) begin
assert(carry);
end

if (cyc == SCYC + 2) begin
assert(result == r);
assert(zero == !r);
assert(carry);
end
end
endmodule
2 changes: 1 addition & 1 deletion tests/alu_bit.sby.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ bmc: mode bmc
append 10
expect pass
multiclock on
bit_bmc: depth 128
bit_bmc: depth 20

[engines]
smtbmc
Expand Down
68 changes: 53 additions & 15 deletions tests/alu_bit.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,23 +4,61 @@
module testbench(input logic clk);
`include "alu.svh"

localparam SCYC = 2;

logic [7:0] a = $anyconst;
logic [2:0] b = $anyconst;

logic [7:0] r;

assign r = a & (1 << b);

always_comb begin
undef_inputs();

/* cyc, opA, opB */
test_bit( 4, 1, 0);
test_bit( 8, 2, 1);
test_bit( 12, 4, 2);
test_bit( 16, 8, 3);
test_bit( 20, 16, 4);
test_bit( 24, 32, 5);
test_bit( 28, 64, 6);
test_bit( 32, 128, 7);
test_bit( 36, 'hfe, 0);
test_bit( 40, 'hf7, 3);
test_bit( 44, 'hef, 4);
test_bit( 48, 'h7f, 7);
test_bit( 52, 'h5a, 0);
test_bit( 56, 'ha5, 7);
line0 = $anyseq;
line0.bs = b;
line0.oe = BS_OE;
line0.lb = BUS_LD;

line1 = $anyseq;
line1.op = a;
line1.sh = NO_SH;
line1.oe = SH_OE;
line1.la = BUS_LD;
line1.lb = NO_LD;
line1.r = 0;
line1.s = 1;
line1.v = 0;
line1.ne = 0;
line1.ci = 1;
line1.l = 1;
line1.h = 0;

line2 = $anyseq;
line2.la = NO_LD;
line2.lb = NO_LD;
line2.r = 0;
line2.s = 1;
line2.v = 0;
line2.ne = 0;
line2.ci = 1;
line2.l = 0;
line2.h = 1;
line2.oe = RES_OE;

if (cyc == SCYC) set_inputs(line0);
if (cyc == SCYC + 1) set_inputs(line1);
if (cyc == SCYC + 2) set_inputs(line2);

if (cyc == SCYC + 1) begin
assert(carry);
end

if (cyc == SCYC + 2) begin
assert(result == r);
assert(zero == !r);
assert(carry);
end
end
endmodule
2 changes: 1 addition & 1 deletion tests/alu_cpl.sby.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ bmc: mode bmc
append 10
expect pass
multiclock on
cpl_bmc: depth 88
cpl_bmc: depth 20

[engines]
smtbmc
Expand Down
60 changes: 50 additions & 10 deletions tests/alu_cpl.sv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,18 +4,58 @@
module testbench(input logic clk);
`include "alu.svh"

localparam SCYC = 2;

logic [7:0] b = $anyconst;

logic [7:0] r;

assign r = ~b;

always_comb begin
undef_inputs();

/* cyc, opB */
test_cpl( 4, 0);
test_cpl( 8, 255);
test_cpl( 12, 1);
test_cpl( 16, 128);
test_cpl( 20, 127);
test_cpl( 24, 'hf0);
test_cpl( 28, 'h0f);
test_cpl( 32, 'haa);
test_cpl( 36, 'h55);
line0 = $anyseq;
line0.op = b;
line0.sh = NO_SH;
line0.oe = SH_OE;
line0.lb = BUS_LD;

line1 = $anyseq;
line1.la = ZERO_LD;
line1.lb = NO_LD;
line1.r = 1;
line1.s = 1;
line1.v = 1;
line1.ne = 1;
line1.ci = 0;
line1.l = 1;
line1.h = 0;

line2 = $anyseq;
line2.la = NO_LD;
line2.lb = NO_LD;
line2.r = 1;
line2.s = 1;
line2.v = 1;
line2.ne = 1;
line2.ci = 0;
line2.l = 0;
line2.h = 1;
line2.oe = RES_OE;

if (cyc == SCYC) set_inputs(line0);
if (cyc == SCYC + 1) set_inputs(line1);
if (cyc == SCYC + 2) set_inputs(line2);

if (cyc == SCYC + 1) begin
assert(!carry);
end

if (cyc == SCYC + 2) begin
assert(result == r);
assert(zero == !r);
assert(!carry);
end
end
endmodule
2 changes: 1 addition & 1 deletion tests/alu_neg.sby.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ bmc: mode bmc
append 10
expect pass
multiclock on
neg_bmc: depth 88
neg_bmc: depth 20

[engines]
smtbmc
Expand Down
Loading

0 comments on commit 74ac11d

Please sign in to comment.