diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2020-11-20 23:31:01 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-23 12:33:19 +0000 |
| commit | c6e261a565e7c4203eae7c34c727dfc911213dca (patch) | |
| tree | 29f8d02af3e5a7656bbcb88ca806d7b280b1dc12 | |
| parent | fa0bf456a70ff69bc749ca92e7a274ec50a47837 (diff) | |
| download | vericert-kvx-michalis.tar.gz vericert-kvx-michalis.zip | |
Add todo for missing logic around instantiationsmichalis
| -rw-r--r-- | src/hls/HTLgen.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index eda025f..c8c5b7e 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/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.") |