diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2020-11-20 23:31:01 +0000 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2020-11-20 23:31:32 +0000 |
| commit | 303a45374643f75698c61f062899973d2c297831 (patch) | |
| tree | ce863c802f71f0665449efb810848a3c817f4281 | |
| parent | a72f26319dabca414a2b576424b9f72afaca161c (diff) | |
| download | vericert-303a45374643f75698c61f062899973d2c297831.tar.gz vericert-303a45374643f75698c61f062899973d2c297831.zip | |
Add todo for missing logic around instantiations
| -rw-r--r-- | src/translation/HTLgen.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index be473fc..8e060e4 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -583,6 +583,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni if Z.leb (Z.pos n') Integers.Int.max_unsigned then do finished <- create_wire 1; do res <- create_wire 32; + (* TODO implement control and datapaths for instantiated module *) add_instance fn args finished res else error (Errors.msg "State is larger than 2^32.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") |