// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // The following module implements a function unit that implements a register // // file that can read and write registers in parallel. // // Note that the events trigger the following basic transport actions: // // ev1: next(r1) = x1 // // ev2: next(r2) = x2 // // ev3: next(r2) = x3 // // ev4: x4 = r4 // // // // ************************************************************************** // macro WL = 8; macro RN = 32; module REG(event ?ev1,?ev2,?ev3,?ev4, bv{WL} ?x1,?x2,?x3,!x4) { [RN]bv{WL} reg; bv{WL} r1,r2,r3,r4; loop { //assert(reg[bv2nat(r1)]==r2 & r4==reg[bv2nat(r3)]); await(ev1 or ev2 or ev3 or ev4); let (v1 = (ev1 ? x1 : r1)) let (v2 = (ev2 ? x2 : r2)) let (v3 = (ev3 ? x3 : r3)) let (v4 = reg[bv2nat(v3)]) { next(r1) = v1; next(r2) = v2; next(r3) = v3; next(r4) = v4; next(reg[bv2nat(v1)]) = v2; if(ev4) x4 = v4; } } }