[lttv.git] / trunk / verif / md / model_03_write_read_off.spin.ltl

// The writer head must always be superior or equal to the reader head.
// assert(write_off - read_off >= 0 && write_off - read_off < HALF_UCHAR);

[] (rwoff1 && rwoff2)
Commit	Line	Data
dc45444e	1	// The writer head must always be superior or equal to the reader head.
	2	// assert(write_off - read_off >= 0 && write_off - read_off < HALF_UCHAR);
	3
	4	[] (rwoff1 && rwoff2)