diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 21:35:34 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 21:35:34 +0000 |
| commit | 359194617de51adcc451b45b6c1b0a9332820906 (patch) | |
| tree | 7b1fce73244ebbb1195c37dd986de0bf1d081a0c /src/hls/FunctionalUnits.v | |
| parent | a47cfd17f0e1fc6aca5e10de9362a4be2d4af468 (diff) | |
| download | vericert-359194617de51adcc451b45b6c1b0a9332820906.tar.gz vericert-359194617de51adcc451b45b6c1b0a9332820906.zip | |
Add new instructions for pipelines
Diffstat (limited to 'src/hls/FunctionalUnits.v')
| -rw-r--r-- | src/hls/FunctionalUnits.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/hls/FunctionalUnits.v b/src/hls/FunctionalUnits.v index 019cf15..392b1ae 100644 --- a/src/hls/FunctionalUnits.v +++ b/src/hls/FunctionalUnits.v @@ -21,13 +21,15 @@ Require Import compcert.lib.Maps. Require Import vericert.common.Vericertlib. +Definition funct_node := positive. + Inductive funct_unit: Type := | SignedDiv (size: positive) (numer denom quot rem: reg): funct_unit | UnsignedDiv (size: positive) (numer denom quot rem: reg): funct_unit. Record funct_units := mk_avail_funct_units { - avail_sdiv: option positive; - avail_udiv: option positive; + avail_sdiv: option funct_node; + avail_udiv: option funct_node; avail_units: PTree.t funct_unit; }. |