Am Freitag, den 11.11.2005, 14:20 -0500 schrieb Timothy Miller: > This is a rewrite of the "basic fifo". The basic fifo can hold 16 > entries and requires input and output clocks to be the same. The sync > fifo allows input and output clocks to be in different domains. It > uses graycode counters for glitch-free crossing of domains for head > and tail pointers. The fifo can only store 15 entries in the memory > buffer, but since the output is registered, it can technically hold > 16. Reset is async so that we don't have to care which clock domain > the signal came from.
I translated the FIFO description into a petri net (see below) for Maria ( http://www.tcs.hut.fi/Software/maria/ ) and played around with it. What I found is a race condition between tail0 and fifo_data. Unless each of the 4 delays between tail0 and valid_out is longer than each of the 32 delays between fifo_data and data_out, the following sequence of events is possible: 0. The FIFO is empty, enq and deq are already set, data_in contains something other than what's already at fifo_data[head0]; 1. in_clock increments tail0 and writes the contents of data_in to fifo_data[head0]; 2. the changed tail0 bit goes through the comparison with head0 and arrives as 1 at the input of valid_data before all 32 bits from fifo_data[head0] arrive at the input of data_out; 3. out_clock sets the output of valid_out to 1, but sets the output of data_out to a mix of old and new values. The state graph can be explored with maria -m fifo.pn -e "visual dumpgraph" Watch out for "read:{*,*,666,true,..." in the third line of state descriptions. // Sync fifo // Copyright 2005, Timothy Miller // Translation to a petri net by Viktor Pracht // LGPL license // Instead of multiple separate gray-coded bools, a single binary-coded // unsigned int is used to index the FIFO. typedef unsigned (0..3) pointer; // WARNING: Since the real data changes multiple bits at a time, this // hides numerous race conditions. typedef unsigned data; // State of the writing clock domain typedef struct { // regs from this clock domain pointer tail0; pointer tail1; pointer tail2; data[pointer] fifo_data; bool full; // inputs from this clock domain bool enq; data data_in; // regs and inputs from other clock domains pointer head0; } write_state; // Propagating inter-domain signals after a write clock edge. typedef enum { tail0, "fifo_data[head0]" } write_signal; // State of the reading clock domain typedef struct { // regs from this clock domain pointer head0; pointer head1; data data_out; bool valid_out; bool _empty; // inputs from this clock domain bool deq; // regs and inputs from other clock domains pointer tail0; data "fifo_data[head0]"; } read_state; // Propagating inter-domain signals after a read clock edge. typedef enum { head0 } read_signal; // Each clock domain is represented by a place for its state, ... place write (1) write_state: {0, 1, 2, {666, 666, 666, 666}, false, true, 42, 0}; // ... a place for currently active outgoing inter-domain signals... place write_active (0..#write_signal) write_signal; ///... and a place for currently inactive outgoing inter-domain signals. place write_inactive (0..#write_signal) write_signal: write_signal s: s; place read (1) read_state: {0, 1, 0, false, true, true, 0, 666}; place read_active (0..#read_signal) read_signal; place read_inactive (0..#read_signal) read_signal: read_signal s: s; // Each 'always' blocks is represented by a transition. trans in_clock // Remove the old state... in { place write: w } // ...and add the new state. out { place write: w.{ fifo_data (!w.full && w.enq ? w.fifo_data.{[w.tail0] w.data_in} : w.fifo_data) }.{ tail0 (!w.full && w.enq ? w.tail1 : w.tail0) }.{ tail1 (!w.full && w.enq ? w.tail2 : w.tail1) }.{ tail2 (!w.full && w.enq ? +w.tail2 : w.tail2) }.{ full (!w.full && w.enq ? w.tail2 == w.head0 : w.tail1 == w.head0) } } // Fire only after all outgoing inter-domain signals had time to // propagate. in { place write_inactive: write_signal s: s } // Make all outgoing inter-domain signals active. out { place write_active: write_signal s: s } ; trans out_clock in { place read: r } out { place read: r.{ data_out (!r.valid_out || r.deq ? r."fifo_data[head0]" : r.data_out) }.{ _empty (!r.valid_out || r.deq ? r.head1 == r.tail0 : r.head0 == r.tail0) }.{ head0 (!(r.head0 == r.tail0) && (!r.valid_out || r.deq) ? r.head1 : r.head0) }.{ head1 (!(r.head0 == r.tail0) && (!r.valid_out || r.deq) ? +r.head1 : r.head1) }.{ valid_out (!(r.head0 == r.tail0) ? true : (r.deq ? false : r.valid_out)) } } in { place read_inactive: read_signal s: s } out { place read_active: read_signal s: s } ; // Signal propagation between clock domains is represented by // transitions. trans head0 in { place read: r; place write: w } out { place read: r; place write: w.{ head0 r.head0 } } // Fire only if this signal is active. in { place read_active: head0 } // Make this signal inactive. out { place read_inactive: head0 } ; trans tail0 in { place read: r; place write: w } out { place read: r.{ tail0 w.tail0 }; place write: w } in { place write_active: tail0 } out { place write_inactive: tail0 } ; trans "fifo_data[head0]" in { place read: r; place write: w } out { place read: r.{ "fifo_data[head0]" w.fifo_data[w.head0] }; place write: w } in { place write_active: "fifo_data[head0]" } out { place write_inactive: "fifo_data[head0]" } ; /* Variable inputs can be represented by transitions, too. trans enq in { place write: w } out { place write: w.{ enq +w.enq } } ; trans data_in in { place write: w } out { place write: w.{ data_in +w.data_in } } ; trans deq in { place read: r } out { place read: r.{ deq +r.deq } } ; */ - Viktor Pracht _______________________________________________ Open-graphics mailing list [email protected] http://lists.duskglow.com/mailman/listinfo/open-graphics List service provided by Duskglow Consulting, LLC (www.duskglow.com)
