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