write test circuit

This commit is contained in:
Fabian Posch 2025-01-09 18:43:15 +01:00
parent f84a62b19f
commit e35f8f0939
5 changed files with 2774 additions and 0 deletions

View file

@ -0,0 +1,136 @@
import std::data;
function ceil_log2 (pint a) : pint
{
pint i;
pint M;
chp {
i := 0;
M := a-1;
*[ M > 0 -> i := i + 1; M := M/2 ];
self := i
}
}
template<pbool reset; pint V; pint N>
defchan gen_a1of <: chan(enum<N>) (std::data::d1of?!<N> d; bool!? a)
{
{ 0 <= V & V < N : "Initial token value out of range" };
methods {
/*-- initialize channel, sender end --*/
send_init {
[ reset -> (,i:N: [ i != V -> d.d[i]- [] else -> d.d[i]+ ])
[] else -> (,i:N: d.d[i]-)
]
}
/*-- set output data --*/
set {
[([]i:N: self = i -> d.d[i]+)]
}
/*-- finish synchronization --*/
send_up {
[a]
}
/*-- reset part of the protocol --*/
send_rest {
(,i:N:d.d[i]-);[~a]
}
/*-- initialize channel, receiver end --*/
recv_init {
a-
}
/*-- get value --*/
get {
[([]i:N:d.d[i] -> self := i)]
}
/*-- finish synchronization action --*/
recv_up {
a+
}
/*-- reset part of the protocol --*/
recv_rest {
[(&i:N:~d.d[i])];a-
}
/*-- probe expression on receiver --*/
recv_probe = (|i:N:d.d[i]);
// no sender probe
}
}
export defchan a1of <: gen_a1of<false,0> () { }
export defchan ar1of <: gen_a1of<true,0> () { }
template<pbool reset; pint V; pint M>
defchan gen_aMx1of2 <: chan(int<M>) (std::data::Mx1of2?!<M> d; bool!? a)
{
{ 0 <= V & ceil_log2(V) < M : "Initial token value out of range" };
methods {
/*-- initialize channel, sender end --*/
send_init {
[ reset -> (,i:M: [ ((V >> i) & 1) = 0 -> d.d[i].f+ [] else -> d.d[i].t+ ])
[] else -> (,i:M: d.d[i].t-,d.d[i].f-)
]
}
/*-- set output data --*/
set {
(,i:M: [((self >> i) & 1) = 0 -> d.d[i].f+ [] else -> d.d[i].t+ ])
}
/*-- finish synchronization --*/
send_up {
[a]
}
/*-- reset part of the protocol --*/
send_rest {
(,i:M: d.d[i].t-,d.d[i].f-);[~a]
}
/*-- initialize channel, receiver end --*/
recv_init {
a-
}
/*-- get value --*/
get {
[(&i:M: d.d[i].t | d.d[i].f)];
self := 0;
(;i:M: [ d.d[i].t -> self := self | (1 << i)
[] else -> skip
]
)
}
/*-- finish synchronization action --*/
recv_up {
a+
}
/*-- reset part of the protocol --*/
recv_rest {
[(&i:M:~d.d[i].t & ~d.d[i].f)];a-
}
/*-- probe expression on receiver --*/
recv_probe = (d.d[0].t|d.d[0].f);
// no sender probe
}
}
export defchan aMx1of2 <: gen_aMx1of2<false,0> () { }
export defchan arMx1of2 <: gen_aMx1of2<true,0> () { }

View file

@ -0,0 +1,19 @@
import "umul4x4.act";
import std::data;
import "minichannel.act";
defproc pipelined_mult(aMx1of2?<4> A, B; aMx1of2!<8> RES; bool? reset) {
pint IN_WIDTH = 4;
pint OUT_WIDTH = 8;
umul4x4 mult;
mult.a = A.d;
mult.ack_out = A.a;
mult.b = B.d;
mult.ack_out = B.a;
RES.d = mult.s;
RES.a = mult.ack_in;
mult.reset = reset;
}

91
test-circuit/simlib.act Normal file
View file

@ -0,0 +1,91 @@
template<pbool INCLUDE_ENABLE; pint D_WIDTH, OUT_CHANNELS, N; pint DATA[N]; pbool LOOP; pint SOURCE_ID; pbool LOG>
defproc source_sequence_multi (chan!(int<D_WIDTH>) O[OUT_CHANNELS]; bool? enable)
{
int i;
int<D_WIDTH> buf;
chp {
// and send it to every channel
(, j : OUT_CHANNELS :
*[
i := 0;
*[ i < N ->
// select the right data element
[([]k:N: i=k -> buf := DATA[k])];
// wait on enable flag
[~INCLUDE_ENABLE|enable];
O[j]!buf;
// if logging was enabled, log the send
[ LOG ->
log ("Source ", SOURCE_ID, " (Channel ", j, "): Sent value ", buf, "%x (0x", buf, ")")
[] else ->
skip
];
i := i + 1
]
<- LOOP ]
);
log ("Source ", SOURCE_ID, ": Sequence ended.")
}
}
template <pint IN_D_WIDTH, OUT_D_WIDTH, IN_CHANNELS, OUT_CHANNELS, SB_ID; pbool VERBOSE_TESTING>
defproc lockstep (chan?(int<IN_D_WIDTH>) IN[IN_CHANNELS]; chan?(int<OUT_D_WIDTH>) OUT_M[OUT_CHANNELS], OUT_D[OUT_CHANNELS])
{
int<IN_D_WIDTH> input[IN_CHANNELS];
int<OUT_D_WIDTH> output_m[OUT_CHANNELS], output_d[OUT_CHANNELS];
bool not_failed;
int num;
chp {
num := 0;
*[
// receive the data
(, i : IN_CHANNELS : IN[i]?input[i]),
(, i : OUT_CHANNELS : OUT_M[i]?output_m[i]),
(, j : OUT_CHANNELS : OUT_D[j]?output_d[j]);
// check the results
not_failed+;
(; i : OUT_CHANNELS : [not_failed -> not_failed := output_m[i] = output_d[i] [] else -> skip]);
// print the output
[ not_failed -> (
// only print successful tests if verbose testing is enabled
[ VERBOSE_TESTING -> (
log_st ("");
log_p ("Scoreboard ", SB_ID, ": TEST SUCCESS (", num, "); inputs {");
(; i : IN_CHANNELS : log_p (i, ": ", input[i], "%x (0x", input[i], "); "));
log_p ("}, outputs {");
(; i : OUT_CHANNELS : log_p (i, ": ", output_d[i], "%x (0x", output_d[i], "); "));
log_p ("}");
log_nl ("")
)
[] else -> (
skip
)]
)
[] else -> (
log_st ("");
log_p ("Scoreboard ", SB_ID, ": TEST FAILED (", num, "); inputs {");
(; i : IN_CHANNELS : log_p (i, ": ", input[i], "%x (0x", input[i], "); "));
log_p ("}, outputs {");
(; i : OUT_CHANNELS : log_p (i, ": expected ", output_m[i], "%x (0x", output_m[i], "), got ", output_d[i], "%x (0x", output_d[i], "); "));
log_p ("}");
log_nl ("")
)];
num := num + 1
]
}
}

View file

@ -0,0 +1,61 @@
import "simlib.act";
import "mult_wrapper.act";
template<pint IN_WIDTH, OUT_WIDTH>
defproc mul_model (chan(int<IN_WIDTH>)? A,B; chan(int<OUT_WIDTH>)! RES; bool res) {
int<IN_WIDTH> a, b;
int<OUT_WIDTH>res;
chp {
*[
[#A];
B?b, A?a;
RES!(a*b)
]
}
}
defproc tb() {
pint IN_WIDTH = 4;
pint OUT_WIDTH = 8;
pint IN_SEQ_L = 8;
pint in_seq_a[IN_SEQ_L];
pint in_seq_b[IN_SEQ_L];
in_seq_a = {7, 6, 5, 1, 2, 3, 0, 4};
in_seq_b = {4, 0, 3, 2, 1, 5, 6, 7};
// model and DUT
mul_model<IN_WIDTH, OUT_WIDTH> model;
pipelined_mult dut;
// simulation harness
lockstep<IN_WIDTH, OUT_WIDTH, 2, 1, 1, true> sb;
source_sequence_multi<true, IN_D_WIDTH, 3, IN_SEQ_L, in_seq_a, true, 1, true> a_src;
source_sequence_multi<true, IN_D_WIDTH, 3, IN_SEQ_L, in_seq_b, true, 2, true> b_src;
// model inputs
model.A = a_src.O[0];
model.B = b_src.O[0];
// DUT inputs
dut.A = a_src.O[1];
dut.b = b_src.O[1];
// scoreboard inputs
sb.IN[0] = a_src[2];
sb.IN[1] = b_src[2];
sb.OUT_M[0] = model.RES;
sb.OUT_D[0] = dut.RES;
chp {
a_src.enable-, b_src.enable-;
dut.reset+;
[after=1000];
dut.reset-;
a_src.enable+, b_src.enable+
}
}

2467
test-circuit/umul4x4.act Normal file

File diff suppressed because it is too large Load diff