diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-08-31 22:37:44 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-31 22:37:44 +0100 |
| commit | b431bdeb59e69df41cd98fadea49968d224493ee (patch) | |
| tree | 2432959ca65908e7c5573d1c87a43be2e8d2d4b4 /src/hls/RTLBlockgen.v | |
| parent | 6cb38f39f5609651691419c6a299b09695a4623c (diff) | |
| download | vericert-b431bdeb59e69df41cd98fadea49968d224493ee.tar.gz vericert-b431bdeb59e69df41cd98fadea49968d224493ee.zip | |
Add working partitioning algorithm
Diffstat (limited to 'src/hls/RTLBlockgen.v')
| -rw-r--r-- | src/hls/RTLBlockgen.v | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v index 05f9a32..6b3e9c3 100644 --- a/src/hls/RTLBlockgen.v +++ b/src/hls/RTLBlockgen.v @@ -24,16 +24,9 @@ From compcert Require Import From vericert Require Import RTLBlock. -Parameter partition : RTL.code -> code. +Parameter partition : RTL.function -> Errors.res function. -Definition transl_function (f : RTL.function) : function := - mkfunction f.(RTL.fn_sig) - f.(RTL.fn_params) - f.(RTL.fn_stacksize) - (partition f.(RTL.fn_code)) - f.(RTL.fn_entrypoint). +Definition transl_fundef := transf_partial_fundef partition. -Definition transl_fundef := transf_fundef transl_function. - -Definition transl_program : RTL.program -> program := - transform_program transl_fundef. +Definition transl_program : RTL.program -> Errors.res program := + transform_partial_program transl_fundef. |