So is it actually necessary to factor out a logic function? I think Yosys ABC takes a global approach anyway. I.e. it would be fine to define boolean transition functions directly. Maybe what I need to do next is to make a layer that is pure, and expresses only boolean functions. Then build state machines on top of that.