Design and verification driven by assertions

In this paper we propose an improvement of the design cycle of synchronous circuits. The use of semi-formal specifications was necessary to write good code and to perform a formal verification using a model checking tool. Our first results show that the implemented code has several advantages with respect to others written with classical methodologies, and we find that formal and functional verification are complementary.