blob: f4f8ce2c55dd4295a28ac06bed138d094d04120f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
+++
title = "Matching states in RTLBlock and RTLPar"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3b"]
forwardlinks = ["3c3b2"]
zettelid = "3c3b1"
+++
One issue is how to match states from the translation from RTLBlock to
RTLPar. Even though the translation is quite straightforward, matching
the states is still quite tricky because of issues with missing
intentional equality between memories and registers.
To match states, we therefore have to ensure that the RTLPar memory is
*extended* from the RTLBlock memory, so that all loads and stores still
result in the same values. In addition to that we need to check that the
register file is *less defined* than the RTLBlock register file.
Finally, stack frames also need to match, which also only have to be
*less defined*.
Finally, we also need to assert that the function was translated using
the translation function that ensures that all the basic blocks succeed
in the validation.
|
