Skip to content

Commit

Permalink
Add some additional test cases
Browse files Browse the repository at this point in the history
  • Loading branch information
Alasdair committed Feb 17, 2025
1 parent 0a37ed5 commit be5a801
Show file tree
Hide file tree
Showing 14 changed files with 221 additions and 0 deletions.
2 changes: 2 additions & 0 deletions test/c/config_register_ones.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
R = 0xFFFFFFFF
R = 0x00000000
18 changes: 18 additions & 0 deletions test/c/config_register_ones.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
default Order dec

$include <prelude.sail>

val ones : forall 'n, 'n >= 0. (implicit('n), unit) -> bits('n)
function ones(n, _) = {
sail_ones(n)
}

register configuration R : bits(32) = ones()

register S : bits(32)

function main(() : unit) -> unit = {
print_bits("R = ", R);
R = sail_zeros(32);
print_bits("R = ", R)
}
3 changes: 3 additions & 0 deletions test/c/dec_str_fixed.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
0x40
0x40
64
12 changes: 12 additions & 0 deletions test/c/dec_str_fixed.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
default Order dec

$include <prelude.sail>
$include <string.sail>

val main : unit -> unit

function main() = {
print_endline(hex_str(64));
print_endline(hex_str_upper(64));
print_endline(dec_str(64));
}
1 change: 1 addition & 0 deletions test/c/eq_anything_union.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ok
20 changes: 20 additions & 0 deletions test/c/eq_anything_union.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
default Order dec

$include <option.sail>
$include <generic_equality.sail>
$include <string.sail>

val main : unit -> unit

function main() = {
let x : option(int) = Some(3);
let y : option(int) = Some(4);
let z : option(int) = None();
assert(x != y);
assert(x != None());
assert(x == Some(3));
assert(z == None());
assert(z == z);
assert(x == x);
print_endline("ok")
}
1 change: 1 addition & 0 deletions test/c/fvec_eq.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ok
13 changes: 13 additions & 0 deletions test/c/fvec_eq.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
default Order dec

$include <prelude.sail>
$include <generic_equality.sail>

val main : unit -> unit

function main() = {
let x = [0x00, 0xFF, 0xAA];
let y = [0x00, 0xFF, 0xAA];
assert(x == y);
print_endline("ok")
}
1 change: 1 addition & 0 deletions test/c/instruction.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ok
109 changes: 109 additions & 0 deletions test/c/instruction.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,109 @@
default Order dec

$include <prelude.sail>
$include <string.sail>

register R1 : bits(32)
register R2 : bits(32)
register R3 : bits(32)
register R4 : bits(32)
register R5 : bits(32)
register R6 : bits(32)
register R7 : bits(32)
register R8 : bits(32)
register R9 : bits(32)
register R10 : bits(32)
register R11 : bits(32)
register R12 : bits(32)
register R13 : bits(32)
register R14 : bits(32)
register R15 : bits(32)


val set_R_int : forall 'n, 0 <= 'n < 16. (int('n), bits(32)) -> unit

function set_R_int(r, x) = {
match r {
0 => (), // zero register
1 => R1 = x,
2 => R2 = x,
3 => R3 = x,
4 => R4 = x,
5 => R5 = x,
6 => R6 = x,
7 => R7 = x,
8 => R8 = x,
9 => R9 = x,
10 => R10 = x,
11 => R11 = x,
12 => R12 = x,
13 => R13 = x,
14 => R14 = x,
15 => R15 = x,
}
}

$[jib_debug]
function set_R(r : bits(4), x : bits(32)) -> unit = {
match r {
0x0 => (), // zero register
0x1 => R1 = x,
0x2 => R2 = x,
0x3 => R3 = x,
0x4 => R4 = x,
0x5 => R5 = x,
0x6 => R6 = x,
0x7 => R7 = x,
0x8 => R8 = x,
0x9 => R9 = x,
0xA => R10 = x,
0xB => R11 = x,
0xC => R12 = x,
0xD => R13 = x,
0xE => R14 = x,
0xF => R15 = x,
}
}

function get_R(r : bits(4)) -> bits(32) = {
match r {
0x0 => 0x0000_0000,
0x1 => R1,
0x2 => R2,
0x3 => R3,
0x4 => R4,
0x5 => R5,
0x6 => R6,
0x7 => R7,
0x8 => R8,
0x9 => R9,
0xA => R10,
0xB => R11,
0xC => R12,
0xD => R13,
0xE => R14,
0xF => R15,
}
}

overload R = {set_R, get_R}

enum iop = {OP_ADD, OP_XOR}

val itype : (bits(12), bits(4), bits(4), iop) -> unit

function itype(imm, rs1, rd, op) = {
let rs1_val = R(rs1);
R(rd) = match op {
OP_ADD => rs1_val + sail_sign_extend(imm, 32),
OP_XOR => xor_vec(rs1_val, sail_sign_extend(imm, 32))
}
}

val main : unit -> unit

function main() = {
set_R_int(4) = 0x0000_0000;
itype(0x000, 0xA, 0xB, OP_ADD);
print_endline("ok")
}
1 change: 1 addition & 0 deletions test/c/list_list_eq.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
ok
16 changes: 16 additions & 0 deletions test/c/list_list_eq.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
default Order dec

$include <prelude.sail>
$include <generic_equality.sail>

val main : unit -> unit

register r : list(list(int)) = [||]

function main() = {
let x : list(list(int)) = [|[|1|], [|2, 3|]|];
r = [|2, 3|] :: [||];
r = [|1|] :: r;
assert(x == r);
print_endline("ok");
}
5 changes: 5 additions & 0 deletions test/c/natural_sort_reg.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
R1 = 0x00000001
R10 = 0x00000002
R2 = 0x00000003
*r = 0x00000002
*r = 0x00000004
19 changes: 19 additions & 0 deletions test/c/natural_sort_reg.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
default Order dec

$include <prelude.sail>

register R1 : bits(32) = 0x0000_0001
register R10 : bits(32) = 0x0000_0002
register R2 : bits(32) = 0x0000_0003

val main : unit -> unit

function main() = {
print_bits("R1 = ", R1);
print_bits("R10 = ", R10);
print_bits("R2 = ", R2);
let r = ref R10;
print_bits("*r = ", *r);
*r = 0x0000_0004;
print_bits("*r = ", *r);
}

0 comments on commit be5a801

Please sign in to comment.