Automated synthesis of crossbars for nanoscale computing using formal methods