I will give a demo of the tool we are developing based on our research about formal analysis of micro-architectures. Going through examples I will illustrate the main modelling and verification features we currently have implemented. An interesting aspect is that we can model asynchronous systems. This part still requires some research and might generate some discussion 🙂