diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-11-18 22:14:30 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-18 22:14:30 +0000 |
| commit | 3c5bd88f22f744e4908afbc5a56e202dfa469360 (patch) | |
| tree | 57ddb252b09bdc61665fcab97ff169acc9af23e7 /src/hls/FunctionalUnits.v | |
| parent | e6348c97faee39754efd13b69a70c54851e2a789 (diff) | |
| download | vericert-3c5bd88f22f744e4908afbc5a56e202dfa469360.tar.gz vericert-3c5bd88f22f744e4908afbc5a56e202dfa469360.zip | |
Fix compilation with new HTL language
Diffstat (limited to 'src/hls/FunctionalUnits.v')
| -rw-r--r-- | src/hls/FunctionalUnits.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/hls/FunctionalUnits.v b/src/hls/FunctionalUnits.v index 9504bb1..dcbe22f 100644 --- a/src/hls/FunctionalUnits.v +++ b/src/hls/FunctionalUnits.v @@ -52,13 +52,11 @@ Record ram := mk_ram { ram_wr_en: reg; ram_d_in: reg; ram_d_out: reg; - ram_ordering: (ram_addr < ram_en - /\ ram_en < ram_d_in - /\ ram_d_in < ram_d_out - /\ ram_d_out < ram_wr_en - /\ ram_wr_en < ram_u_en) }. +Definition all_ram_regs r := + ram_mem r::ram_en r::ram_u_en r::ram_addr r::ram_wr_en r::ram_d_in r::ram_d_out r::nil. + Inductive funct_unit: Type := | SignedDiv: divider true -> funct_unit | UnsignedDiv: divider false -> funct_unit |