From d6f2303568dd45b5c684612482485b4a46da1d88 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Sun, 2 May 2021 12:49:18 +0100 Subject: Give a (questionable) translation spec for HTLgen I am not yet convinced it is the right one, particularly around the way I've used existentials. I will be updating it as I progress with the proof. --- src/hls/HTLgen.v | 64 ++++++++++++++++++++++++++++++---------------------- src/hls/HTLgenspec.v | 36 +++++++++++++++++++---------- 2 files changed, 61 insertions(+), 39 deletions(-) (limited to 'src') diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index a3c0ca6..5f9e17d 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -461,26 +461,28 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := end) (enumerate 0 ns). -(** [mk_fork] creates a datapath statement which sets up the execution of a *) -Definition mk_fork (m : ident) (args : list reg) : mon datapath_stmnt := - do reset_reg <- map_externctrl m ctrl_reset; - do param_assigns <- traverselist - (fun (a: (nat * reg)) => let (idx, arg) := a in - do param_reg <- map_externctrl m (ctrl_param idx); - ret (Vnonblock (Vvar param_reg) (Vvar arg))) - (enumerate 0 args); - let reset_mod := Vnonblock (Vvar reset_reg) (posToLit 1) in +(** [fork] a datapath statement which sets up the execution of a function *) +Definition fork (rst : reg) (params : list (reg * reg)) : datapath_stmnt := + let reset_mod := Vnonblock (Vvar rst) (posToLit 1) in let assign_params := - List.fold_left (fun (acc : stmnt) (s : stmnt) => Vseq acc s) - param_assigns Vskip in - ret (Vseq reset_mod assign_params). + List.fold_left (fun acc (a : reg*reg) => let (dst, src) := a in Vseq (nonblock dst (Vvar src)) acc) + params Vskip in + Vseq reset_mod assign_params. -Definition mk_join (m : ident) (dst : reg) : mon datapath_stmnt := - do return_reg <- map_externctrl m ctrl_return; - do reset_reg <- map_externctrl m ctrl_reset; - let set_result := Vnonblock (Vvar dst) (Vvar return_reg) in - let stop_reset := Vnonblock (Vvar reset_reg) (Vlit (ZToValue 0)) in - ret (Vseq stop_reset set_result). +Definition join (fn_rtrn fn_rst fn_dst : reg) : datapath_stmnt := + let set_result := Vnonblock (Vvar fn_dst) (Vvar fn_rtrn) in + let stop_reset := Vnonblock (Vvar fn_rst) (Vlit (ZToValue 0)) in + Vseq stop_reset set_result. + +Definition return_val fin rtrn r := + let retval := + match r with + | Some r' => Vvar r' + | None => Vlit (ZToValue 0%Z) + end in + Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn retval). + +Definition idle fin := nonblock fin (Vlit (ZToValue 0%Z)). Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with @@ -511,12 +513,24 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Icall sig (inr fn) args dst n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then do _ <- declare_reg None dst 32; - do finish_reg <- map_externctrl fn ctrl_finish; do join_state <- create_state; - do fork_instr <- mk_fork fn args; - do join_instr <- mk_join fn dst; + + do finish_reg <- map_externctrl fn ctrl_finish; + do reset_reg <- map_externctrl fn ctrl_reset; + do return_reg <- map_externctrl fn ctrl_return; + + do params <- traverselist + (fun (a: nat * reg) => let (idx, arg) := a in + do param_reg <- map_externctrl fn (ctrl_param idx); + ret (param_reg, arg)) + (enumerate 0 args); + + let fork_instr := fork reset_reg params in + let join_instr := join return_reg reset_reg dst in + do _ <- add_instr n join_state fork_instr; add_instr_wait finish_reg join_state n' join_instr + else error (Errors.msg "State is larger than 2^32.") | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") @@ -531,12 +545,8 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni error (Errors.msg "Ijumptable: Case statement not supported.") | Ireturn r => do idle_state <- create_state; - let retval := match r with - | Some r' => Vvar r' - | None => Vlit (ZToValue 0%Z) - end in - do _ <- add_instr n idle_state (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn retval)); - add_instr_skip idle_state (nonblock fin (Vlit (ZToValue 0%Z))) + do _ <- add_instr n idle_state (return_val fin rtrn r); + add_instr_skip idle_state (idle fin) end end. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index f3c375c..51a5206 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -125,6 +125,7 @@ Ltac monadInv H := statemachine that is created by the translation contains the correct translations for each of the elements *) +(** [tr_instr] describes the translation of instructions that are directly translated into a single state *) Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt -> control_stmnt -> Prop := | tr_instr_Inop : forall n, @@ -135,23 +136,12 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> datapath_stmnt - Z.pos n <= Int.max_unsigned -> translate_instr op args s = OK e s' i -> tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) -(* | tr_instr_Icall : *) -(* forall n sig fn args dst, *) -(* Z.pos n <= Int.max_unsigned -> *) -(* tr_instr fin rtrn st stk (RTL.Icall sig (inr fn) args dst n) (HTLfork fn args) (state_goto st n) *) | tr_instr_Icond : forall n1 n2 cond args s s' i c, Z.pos n1 <= Int.max_unsigned -> Z.pos n2 <= Int.max_unsigned -> translate_condition cond args s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) -(* | tr_instr_Ireturn_None : *) -(* tr_instr fin rtrn st stk (RTL.Ireturn None) (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) *) -(* (block rtrn (Vlit (ZToValue 0%Z))))) (ctrl_vstmnt Vskip) *) -(* | tr_instr_Ireturn_Some : *) -(* forall r, *) -(* tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) *) -(* (data_vstmnt (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r)))) (ctrl_vstmnt Vskip) *) | tr_instr_Iload : forall mem addr args s s' i c dst n, Z.pos n <= Int.max_unsigned -> @@ -171,12 +161,34 @@ Hint Constructors tr_instr : htlspec. Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts : datapath) (trans : controllogic) (fin rtrn st stk : reg) : Prop := - tr_code_intro : +| tr_code_single : forall s t, c!pc = Some i -> stmnts!pc = Some s -> trans!pc = Some t -> tr_instr fin rtrn st stk i s t -> + tr_code c pc i stmnts trans fin rtrn st stk +| tr_code_call : + forall sig fn args dst n, + c!pc = Some (RTL.Icall sig (inr fn) args dst n) -> + Z.pos n <= Int.max_unsigned -> + + (exists pc2 fn_rst fn_return fn_finish fn_params, + stmnts!pc = Some (fork fn_rst (List.combine fn_params args)) -> + trans!pc = Some (state_goto st pc2) -> + stmnts!pc2 = Some (join fn_return fn_rst dst) -> + trans!pc2 = Some (state_wait st fn_finish n)) -> + + tr_code c pc i stmnts trans fin rtrn st stk +| tr_code_return : + forall r, + c!pc = Some (RTL.Ireturn r) -> + (exists pc2, + stmnts!pc = Some (return_val fin rtrn r) -> + trans!pc = Some (state_goto st pc2) -> + stmnts!pc2 = Some (idle fin) -> + trans!pc2 = Some Vskip) -> + tr_code c pc i stmnts trans fin rtrn st stk. Hint Constructors tr_code : htlspec. -- cgit