Formality and hard Lefschetz property of aspherical manifolds

For a Lie group $G={\mathbb{R}}^n{⋉}_{\varphi }{\mathbb{R}}^m$ with the semi-simple action $\varphi :{\mathbb{R}}^n\to \mathrm{A}\mathrm{u}\mathrm{t}({\mathbb{R}}^m)$, we show that if $\mathrm{\Gamma }$ is a finite extension of a lattice of $G$ then $K(\mathrm{\Gamma },1)$ is formal. Moreover we show that a compact symplectic aspherical manifold with the fundamental group $\mathrm{\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.