From d3c9c0f5659d9c97f09f4aaa4d0e9bede9ce3e2b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 22 Oct 2020 09:55:47 +0200 Subject: attempt at modeling Rocket --- riscV/OpWeights.ml | 83 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) (limited to 'riscV/OpWeights.ml') diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml index 143435c1..637f2904 100644 --- a/riscV/OpWeights.ml +++ b/riscV/OpWeights.ml @@ -1,5 +1,87 @@ open Op;; +(* Attempt at modeling the Rocket core *) + +let resource_bounds = [| 1 |];; +let nr_non_pipelined_units = 1;; (* divider *) + +let latency_of_op (op : operation) (nargs : int) = + match op with + | Omul | Omulhs | Omulhu + | Omull | Omullhs | Omullhu -> 4 + + | Onegf -> 1 (*r [rd = - r1] *) + | Oabsf (*r [rd = abs(r1)] *) + | Oaddf (*r [rd = r1 + r2] *) + | Osubf (*r [rd = r1 - r2] *) + | Omulf -> 6 (*r [rd = r1 * r2] *) + | Onegfs -> 1 (*r [rd = - r1] *) + | Oabsfs (*r [rd = abs(r1)] *) + | Oaddfs (*r [rd = r1 + r2] *) + | Osubfs (*r [rd = r1 - r2] *) + | Omulfs -> 4 (*r [rd = r1 * r2] *) + | Osingleoffloat (*r [rd] is [r1] truncated to single-precision float *) + | Ofloatofsingle -> 4 (*r [rd] is [r1] extended to double-precision float *) +(*c Conversions between int and float: *) + | Ointoffloat (*r [rd = signed_int_of_float64(r1)] *) + | Ointuoffloat (*r [rd = unsigned_int_of_float64(r1)] *) + | Ofloatofint (*r [rd = float64_of_signed_int(r1)] *) + | Ofloatofintu -> 6 (*r [rd = float64_of_unsigned_int(r1)] *) + | Ointofsingle (*r [rd = signed_int_of_float32(r1)] *) + | Ointuofsingle (*r [rd = unsigned_int_of_float32(r1)] *) + | Osingleofint (*r [rd = float32_of_signed_int(r1)] *) + | Osingleofintu -> 4 (*r [rd = float32_of_unsigned_int(r1)] *) + | Olongoffloat (*r [rd = signed_long_of_float64(r1)] *) + | Olonguoffloat (*r [rd = unsigned_long_of_float64(r1)] *) + | Ofloatoflong (*r [rd = float64_of_signed_long(r1)] *) + | Ofloatoflongu -> 6 (*r [rd = float64_of_unsigned_long(r1)] *) + | Olongofsingle (*r [rd = signed_long_of_float32(r1)] *) + | Olonguofsingle (*r [rd = unsigned_long_of_float32(r1)] *) + | Osingleoflong (*r [rd = float32_of_signed_long(r1)] *) + | Osingleoflongu -> 4 (*r [rd = float32_of_unsigned_int(r1)] *) + + | Odiv | Odivu | Odivl | Odivlu -> 16 + | Odivfs -> 35 + | Odivf -> 50 + + | Ocmp cond -> + (match cond with + | Ccomp _ + | Ccompu _ + | Ccompimm _ + | Ccompuimm _ + | Ccompl _ + | Ccomplu _ + | Ccomplimm _ + | Ccompluimm _ -> 1 + | Ccompf _ + | Cnotcompf _ -> 6 + | Ccompfs _ + | Cnotcompfs _ -> 4) + | _ -> 1;; + +let resources_of_op (op : operation) (nargs : int) = resource_bounds;; + +let non_pipelined_resources_of_op (op : operation) (nargs : int) = + match op with + | Odiv | Odivu -> [| 29 |] + | Odivfs -> [| 20 |] + | Odivl | Odivlu | Odivf -> [| 50 |] + | _ -> [| -1 |];; + +let resources_of_cond (cond : condition) (nargs : int) = resource_bounds;; + +let latency_of_load trap chunk (addr : addressing) (nargs : int) = 3;; +let latency_of_call _ _ = 6;; + +let resources_of_load trap chunk addressing nargs = resource_bounds;; + +let resources_of_store chunk addressing nargs = resource_bounds;; + +let resources_of_call _ _ = resource_bounds;; +let resources_of_builtin _ = resource_bounds;; + +(* (* Attempt at modeling SweRV EH1 [| issues ; LSU ; multiplier |] *) let resource_bounds = [| 2 ; 1; 1 |];; @@ -37,3 +119,4 @@ let resources_of_store chunk addressing nargs = [| 1; 1; 0 |];; let resources_of_call _ _ = resource_bounds;; let resources_of_builtin _ = resource_bounds;; + *) -- cgit