[adam_walker]

I'll have to think about that one. TBH, this stuff is pretty difficult to reason about.

However, I can say that I used a SMT solver as part of the wonderful SymbiYosys verification flow to verify that the design was good for around 20 cycles, no matter what the inputs are. That, and the randomised testing gives me quite a bit of confidence in the design.

[plagiarist]

I'd trust the SMT solver also! But if I read correctly you were only doing one insert at a time thus far? If you give it a try with multiple I hope you post again! This was a really neat project to read.