Formality and hard Lefschetz property of aspherical manifolds

For a Lie group $G=\R^{n}\ltimes_{\phi}\R^{m}$ with the semi-simple action $\phi:\R^{n}\to {\rm Aut}(\R^{m})$, we show that if $\Gamma$ is a finite extension of a lattice of $G$ then $K(\Gamma, 1)$ is formal. Moreover we show that a compact symplectic aspherical manifold with the fundamental group $\Gamma$ satisfies the hard Lefschetz property. By those results we give many examples of formal solvmanifolds satisfying the hard Lefschetz property but not admitting K\"ahler structures.