SMT Backend: move undefined memory behavior modelling to firrtl IR level (#2095)

With this PR the smt backend now supports memories
with more than two write ports and the conservative
memory modelling can be selectively turned off with
a new annotation.