I wrote an assertion that states:
If ddtc_miss(sva internal signal) rises then in the same cycle ddt_walk should go high as well.
Below is the counter-example of the assertion failure, you can see that ddtc_miss rises in cycle 16 but ddt_walk didn't rise here. After doing a "why analysis" I found the reason for assertion failure. The reason for the failure is that while loading dc when we have a translation of pdtp.ppn, trans_type is UNTRANSLATED_RX and pte.x == 0 that should result in a page fault exception but IOMMU asserted the updated_dc_o signal which is wrong.
I wrote an assertion that states:
Below is the counter-example of the assertion failure, you can see that
ddtc_missrises in cycle 16 butddt_walkdidn't rise here. After doing a "why analysis" I found the reason for assertion failure. The reason for the failure is that while loading dc when we have a translation of pdtp.ppn, trans_type is UNTRANSLATED_RX and pte.x == 0 that should result in a page fault exception but IOMMU asserted theupdated_dc_osignal which is wrong.