Hi Everyone,
The initial integration of CBMC (C Bounded Model checking) for TF-RMM has been merged. Please refer to the application note here for more details on how to trigger CBMC analysis/coverage/assert targets on TF-RMM implementation :
https://tf-rmm.readthedocs.io/en/latest/resources/application-notes/cbmc.html
Best Regards
Soby Mathew