>>         LEAF(mips1_wbflush)
>>                 lui     v0, 0x8000
>>                 lw      v0, 0(v0)
>>                 j       ra
>>                 nop
>>                 END(mips1_wbflush)
>
> This should be 0xa000 (uncached) to get the desired result.

Ahh, of course it is.

> Do we want the call in question to only flush the processor write
> buffer,

I intended to flush on chip writebutter.

Tohru Nishimura