diff options
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 |