Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 16 additions & 10 deletions specs/fpga/testbench/router_tb.t27
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,8 @@ module Router_Testbench {
var test_failed : u32 = 0;

fn tick() {
clk = false;
clk = true;
// Toggle clock signal for one clock cycle
clk = !clk;
}

fn reset() {
Expand Down Expand Up @@ -55,48 +55,54 @@ module Router_Testbench {
return (nets * 100) / capacity;
}

test test_reset_state {
test "test_reset_state" {
reset();
invariant route_done == false;
invariant route_valid == false;
}

test test_manhattan_distance_zero {
test "test_manhattan_distance_zero" {
var d : u32 = manhattan_distance(0, 0, 0, 0);
invariant d == 0;
}

test test_manhattan_distance_simple {
test "test_manhattan_distance_simple" {
var d : u32 = manhattan_distance(0, 0, 3, 4);
invariant d == 7;
}

test test_manhattan_distance_symmetric {
test "test_manhattan_distance_symmetric" {
var d1 : u32 = manhattan_distance(1, 2, 5, 8);
var d2 : u32 = manhattan_distance(5, 8, 1, 2);
invariant d1 == d2;
}

test test_wire_length_estimate {
test "test_wire_length_estimate" {
var wl : u32 = estimate_wire_length(16, 10);
invariant wl > 0;
}

test test_congestion_low {
test "test_congestion_low" {
var c : u32 = congestion_factor(10, 100);
invariant c == 10;
}

test test_congestion_full {
test "test_congestion_full" {
var c : u32 = congestion_factor(100, 100);
invariant c == 100;
}

test test_grid_size {
test "test_grid_size" {
invariant GRID_SIZE == 16;
invariant NUM_LAYERS == 2;
}

test "test_tick" {
var initial_clk : bool = clk;
tick();
invariant clk != initial_clk;
}

invariant grid_positive : GRID_SIZE > 0;
invariant layers_positive : NUM_LAYERS > 0;

Expand Down
Loading