diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-06 18:59:07 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-06 18:59:07 +0000 |
| commit | da34700998cbaf705c761a3d5b3a4e14994623e4 (patch) | |
| tree | 84b7f00d68a2efaaef16abd32a9f642b654c0c03 /src/SoftwarePipelining/SPBasic.ml | |
| parent | 67c0250258e3d38faf06c755efb2aa556b4ebe79 (diff) | |
| download | vericert-da34700998cbaf705c761a3d5b3a4e14994623e4.tar.gz vericert-da34700998cbaf705c761a3d5b3a4e14994623e4.zip | |
Add comments to pipelining code
Diffstat (limited to 'src/SoftwarePipelining/SPBasic.ml')
| -rw-r--r-- | src/SoftwarePipelining/SPBasic.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/SoftwarePipelining/SPBasic.ml b/src/SoftwarePipelining/SPBasic.ml index df7342f..32234b8 100644 --- a/src/SoftwarePipelining/SPBasic.ml +++ b/src/SoftwarePipelining/SPBasic.ml @@ -1,5 +1,5 @@ (***********************************************************************) -(* *) + (* *) (* Compcert Extensions *) (* *) (* Jean-Baptiste Tristan *) @@ -604,12 +604,12 @@ let latency n = (* A raffiner *) | Omove -> 1 (*| Oaddimm _ -> 1*) (*| Oadd -> 2*) - | Omul -> 3 + | Omul -> 4 | Odiv -> 30 - | Omulimm _ -> 5 + | Omulimm _ -> 4 | _ -> 2 end - | Iload _ -> 10 + | Iload _ -> 1 (* | Ialloc _ -> 20*) | _ -> 1 |