diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-03-01 15:50:26 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-03-01 15:50:26 +0000 |
| commit | a90265c71d6d5c5ec031a8385f977c050bdd7975 (patch) | |
| tree | b10176eea3ee1b4a55c81bc5c7de53bfad8e994c /src/hls/FunctionalUnits.v | |
| parent | 975a5fb0c11af6e8db3f250322794c0712f4af90 (diff) | |
| download | vericert-a90265c71d6d5c5ec031a8385f977c050bdd7975.tar.gz vericert-a90265c71d6d5c5ec031a8385f977c050bdd7975.zip | |
Finish initial implementation of memory gen
Diffstat (limited to 'src/hls/FunctionalUnits.v')
| -rw-r--r-- | src/hls/FunctionalUnits.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/hls/FunctionalUnits.v b/src/hls/FunctionalUnits.v index 019cf15..e4d51b3 100644 --- a/src/hls/FunctionalUnits.v +++ b/src/hls/FunctionalUnits.v @@ -23,19 +23,22 @@ Require Import vericert.common.Vericertlib. Inductive funct_unit: Type := | SignedDiv (size: positive) (numer denom quot rem: reg): funct_unit -| UnsignedDiv (size: positive) (numer denom quot rem: reg): funct_unit. +| UnsignedDiv (size: positive) (numer denom quot rem: reg): funct_unit +| Ram (size: positive) (addr d_in d_out wr_en: reg): funct_unit. Record funct_units := mk_avail_funct_units { avail_sdiv: option positive; avail_udiv: option positive; + avail_ram: option positive; avail_units: PTree.t funct_unit; }. Definition initial_funct_units := - mk_avail_funct_units None None (PTree.empty funct_unit). + mk_avail_funct_units None None None (PTree.empty funct_unit). Definition funct_unit_stages (f: funct_unit) : positive := match f with | SignedDiv s _ _ _ _ => s | UnsignedDiv s _ _ _ _ => s + | _ => 1 end. |