diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-01 13:25:38 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-01 13:25:38 +0100 |
| commit | 5587a3a45d9fb706e97f13b836fe4021179d1aeb (patch) | |
| tree | 565fe4ee31d2c0f68472b645228cd1e7d58c6eb1 | |
| parent | 6b7f0ddcf16d6a4e3629cfc19af3de7253d65f15 (diff) | |
| download | vericert-5587a3a45d9fb706e97f13b836fe4021179d1aeb.tar.gz vericert-5587a3a45d9fb706e97f13b836fe4021179d1aeb.zip | |
Give more specific reasons for Renaming failing
| -rw-r--r-- | src/hls/Renaming.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/hls/Renaming.v b/src/hls/Renaming.v index 9062e13..ab14ba4 100644 --- a/src/hls/Renaming.v +++ b/src/hls/Renaming.v @@ -187,7 +187,11 @@ Definition renumber_module (m : HTL.module) : mon HTL.module := MORD WFRAM WFPARAMS) - | _, _, _, _, _ => error (Errors.msg "More than 2^32 states.") + | right _, _, _, _, _ => error (Errors.msg "Renaming: More than 2^32 datapath states") + | _, right _, _, _, _ => error (Errors.msg "Renaming: More than 2^32 controlpath states") + | _, _, right _, _, _ => error (Errors.msg "Renaming: Incorrect ordering of control registers") + | _, _, _, right _, _ => error (Errors.msg "Renaming: Parameter registers conflict with control registers") + | _, _, _, _, None => error (Errors.msg "Renaming: Ram address register conflicts with control registers") end. Definition renumber_fundef (fundef : HTL.fundef) : mon HTL.fundef := |