diff options
-rw-r--r-- | verilog.tex | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/verilog.tex b/verilog.tex index 015d462..b0af602 100644 --- a/verilog.tex +++ b/verilog.tex @@ -125,11 +125,13 @@ The Verilog semantics do not define a memory model for Verilog, as this is not n %\JW{I'm not quite sure I understand. Let me check: Are you saying that previous work has shown how all the existing CompCert passes can be adapted from an infinite to a finite memory model, but what we're doing is leaving the default (infinite) memory model for the CompCert front end, and just converting from an infinite memory model to a finite memory model when we go from 3AC to HTL?}\YH{Yes exactly, most papers changed the whole memory model to thread through properties that were then needed in the back end, but we currently don't need to do that. I need to double check though for CompCertELF, it doesn't actually seem to be the case. Will edit this section later.} +\definecolor{compcertmemmodel}{HTML}{e2ccea} +\definecolor{vericertmemmodel}{HTML}{cbe1db} \begin{figure} \centering \begin{tikzpicture} - \draw (0,0) rectangle (5,-5); - \draw (7,0) rectangle (12,-5); + \fill[compcertmemmodel,rounded corners=3pt] (0,0) rectangle (5,-4.3); + \fill[vericertmemmodel,rounded corners=3pt] (7,0) rectangle (12,-4.3); \node[right] at (0,-0.3) {\small \textbf{\compcert{}'s Memory Model}}; \node[right] at (7,-0.3) {\small \textbf{Verilog Memory Representation}}; \node[right] (x0) at (0.2,-1.9) {\small 0}; |