Property for when writes to a fifo stop

I need a property for formal analysis that says when writes to a FIFO stop, the FIFO eventually empties.  The logic in the module I am verifying does the reading of the FIFO.  I'm trying to verify that the logic will always read everything out.  The write is an input to the module.

I broke it up into an assumption and an assertion.  Let me know if you think this works or if you have a better idea.  Thanks.

//psl assume_wr_stops: assume always(
// eventually! ~write
//)@(posedge clk);

//psl assert_eventually_empty: assert always(
// eventually! empty
//)@(posedge clk);