diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-22 18:42:11 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-22 18:42:11 +0000 |
| commit | 2243443c407a1e951265a9252bac3d3b9b830cbb (patch) | |
| tree | 80ad4560456aa30abc2c1a01b09a86c4ece7b6e9 /src/hls/RTLPargen.v | |
| parent | 1a7f581dc4b67cbfe17936697aec8f85786c844d (diff) | |
| download | vericert-2243443c407a1e951265a9252bac3d3b9b830cbb.tar.gz vericert-2243443c407a1e951265a9252bac3d3b9b830cbb.zip | |
Fix arguments to RBassign and piped
Diffstat (limited to 'src/hls/RTLPargen.v')
| -rw-r--r-- | src/hls/RTLPargen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 97ec9aa..aaabe5d 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -577,7 +577,7 @@ Definition update (f : forest) (i : instr) : forest := f # Mem <- (Estore (f # Mem) chunk addr (list_translation rl f) (f # (Reg r))) | RBsetpred c addr p => f | RBpiped p fu args => f - | RBassign p fu dst => f + | RBassign p fu src dst => f end. (*| |