diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-20 21:02:24 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-20 21:02:24 +0100 |
commit | 7a05aa21b3a94842ceaf103a53209d87d7f095d5 (patch) | |
tree | 31ab96aa633b0a972fb719ab3318e24654e464b2 /src/hls/HTLgen.v | |
parent | 7183a0a0a037026a0d03e4df6153ca2d5879af49 (diff) | |
download | vericert-7a05aa21b3a94842ceaf103a53209d87d7f095d5.tar.gz vericert-7a05aa21b3a94842ceaf103a53209d87d7f095d5.zip |
Move renumbering to be HTL->HTL
Diffstat (limited to 'src/hls/HTLgen.v')
-rw-r--r-- | src/hls/HTLgen.v | 213 |
1 files changed, 213 insertions, 0 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index a12b7f9..9347f39 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -28,6 +28,7 @@ Require Import compcert.backend.RTL. Require Import vericert.common.Statemonad. Require Import vericert.common.Vericertlib. +Require Import vericert.common.Maps. Require Import vericert.hls.AssocMap. Require Import vericert.hls.HTL. Require Import vericert.hls.ValueInt. @@ -652,6 +653,218 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program := (fun i v => Errors.OK v) p. *) +Record renumber_state: Type := + mk_renumber_state { + renumber_freshreg : reg; + renumber_regmap : PTree.t reg; + renumber_clk : reg; + }. + +Module RenumberState <: State. + Definition st := renumber_state. + + Definition st_prop (st1 st2 : st) := renumber_clk st1 = renumber_clk st2. + + Lemma st_refl : forall (s : st), st_prop s s. + Proof. constructor. Qed. + + Lemma st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. + Proof. congruence. Qed. +End RenumberState. + +Module RenumberMonad := Statemonad(RenumberState). +Module RenumberMonadExtra := Monad.MonadExtra(RenumberMonad). + +Section RENUMBER. + Import RenumberMonad. + Import RenumberState. + Import RenumberMonadExtra. + Import MonadNotation. + + Program Definition map_reg (r: reg) : mon reg := + fun st => OK + (renumber_freshreg st) + (mk_renumber_state (Pos.succ (renumber_freshreg st)) + (PTree.set r (renumber_freshreg st) (renumber_regmap st)) + (renumber_clk st)) + _. + Next Obligation. unfold st_prop; auto. Qed. + + Program Definition clear_mapping : mon unit := + fun st => OK + tt + (mk_renumber_state (renumber_freshreg st) + (PTree.empty reg) + (renumber_clk st)) + _. + Next Obligation. unfold st_prop; auto. Qed. + + Definition renumber_reg (r : reg) : mon reg := + do st <- get; + match PTree.get r (renumber_regmap st) with + | Some reg' => ret reg' + | None => map_reg r + end. + + Definition get_clk : mon reg := do st <- get; ret (renumber_clk st). + + Fixpoint renumber_expr (expr : Verilog.expr) := + match expr with + | Vlit val => ret (Vlit val) + | Vvar reg => + do reg' <- renumber_reg reg; + ret (Vvar reg') + | Vvari reg e => + do reg' <- renumber_reg reg; + do e' <- renumber_expr e; + ret (Vvari reg' e') + | Vinputvar reg => + do reg' <- renumber_reg reg; + ret (Vvar reg') + | Vbinop op e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vbinop op e1' e2') + | Vunop op e => + do e' <- renumber_expr e; + ret (Vunop op e') + | Vternary e1 e2 e3 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + do e3' <- renumber_expr e3; + ret (Vternary e1' e2' e3') + | Vrange r e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + do r' <- renumber_reg r; + ret (Vrange r e1' e2') + end. + + Fixpoint renumber_stmnt (stmnt : Verilog.stmnt) := + match stmnt with + | Vskip => ret Vskip + | Vseq s1 s2 => + do s1' <- renumber_stmnt s1; + do s2' <- renumber_stmnt s2; + ret (Vseq s1' s2') + | Vcond e s1 s2 => + do e' <- renumber_expr e; + do s1' <- renumber_stmnt s1; + do s2' <- renumber_stmnt s2; + ret (Vcond e' s1' s2') + | Vcase e cs def => + do e' <- renumber_expr e; + do cs' <- sequence (map + (fun (c : (Verilog.expr * Verilog.stmnt)) => + let (c_expr, c_stmnt) := c in + do expr' <- renumber_expr c_expr; + do stmnt' <- renumber_stmnt c_stmnt; + ret (expr', stmnt')) cs); + do def' <- match def with + | None => ret None + | Some d => do def' <- renumber_stmnt d; ret (Some def') + end; + ret (Vcase e' cs' def') + | Vblock e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vblock e1' e2') + | Vnonblock e1 e2 => + do e1' <- renumber_expr e1; + do e2' <- renumber_expr e2; + ret (Vnonblock e1' e2') + end. + + Definition renumber_module (m : HTL.module) : mon HTL.module := + do mod_start' <- renumber_reg (HTL.mod_start m); + do mod_reset' <- renumber_reg (HTL.mod_reset m); + do mod_clk' <- get_clk; + do mod_finish' <- renumber_reg (HTL.mod_finish m); + do mod_return' <- renumber_reg (HTL.mod_return m); + do mod_st' <- renumber_reg (HTL.mod_st m); + do mod_stk' <- renumber_reg (HTL.mod_stk m); + do mod_params' <- traverselist renumber_reg (HTL.mod_params m); + do mod_controllogic' <- traverse_ptree1 renumber_stmnt (HTL.mod_controllogic m); + do mod_datapath' <- traverse_ptree1 renumber_stmnt (HTL.mod_datapath m); + + do _ <- clear_mapping; + + match zle (Z.pos (max_pc_map mod_datapath')) Integers.Int.max_unsigned, + zle (Z.pos (max_pc_map mod_controllogic')) Integers.Int.max_unsigned with + | left LEDATA, left LECTRL => + ret (HTL.mkmodule + mod_params' + mod_datapath' + mod_controllogic' + (HTL.mod_entrypoint m) + mod_st' + (HTL.mod_stk m) + (HTL.mod_stk_len m) + mod_finish' + mod_return' + mod_start' + mod_reset' + mod_clk' + (HTL.mod_scldecls m) + (HTL.mod_arrdecls m) + (HTL.mod_externctrl m) + (conj (max_pc_wf _ _ LECTRL) (max_pc_wf _ _ LEDATA))) + | _, _ => error (Errors.msg "More than 2^32 states.") + end. + + Definition renumber_fundef (fundef : HTL.fundef) : mon HTL.fundef := + match fundef with + | Internal m => do renumbered <- renumber_module m; ret (Internal renumbered) + | _ => ret fundef + end. + + Section TRANSF_PROGRAM_STATEFUL. + Import RenumberMonad. + Import RenumberState. + Import RenumberMonadExtra. + Import MonadNotation. + + Variables A B V : Type. + Variable transf_fun: ident -> A -> RenumberMonad.mon B. + + Fixpoint transf_globdefs (l: list (ident * globdef A V)) : RenumberMonad.mon (list (ident * globdef B V)) := + match l with + | nil => RenumberMonad.ret nil + | (id, Gfun f) :: l' => + do tf <- transf_fun id f; + do tl' <- transf_globdefs l'; + RenumberMonad.ret ((id, Gfun tf) :: tl') + | (id, Gvar v) :: l' => + do tl' <- transf_globdefs l'; + RenumberMonad.ret ((id, Gvar v) :: tl') + end. + + Definition transform_stateful_program (init_state : RenumberState.st) (p: AST.program A V) : Errors.res (AST.program B V) := + RenumberMonad.run_mon init_state ( + do gl' <- transf_globdefs p.(prog_defs); + RenumberMonad.ret (mkprogram gl' p.(prog_public) p.(prog_main))). + + End TRANSF_PROGRAM_STATEFUL. + + Definition get_main_clk (p : HTL.program) : Errors.res reg := + let ge := Globalenvs.Genv.globalenv p in + match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with + | Some b => + match Globalenvs.Genv.find_funct_ptr ge b with + | Some (AST.Internal m) => Errors.OK (HTL.mod_clk m) + | _ => Errors.Error (Errors.msg "Cannot find internal main for renumbering") + end + | _ => Errors.Error (Errors.msg "Cannot find internal main for renumbering") + end. + + Definition renumber_program (p : HTL.program) : Errors.res HTL.program := + Errors.bind (get_main_clk p) + (fun main_clk => transform_stateful_program _ _ _ + (fun _ => renumber_fundef) + (mk_renumber_state 1%positive (PTree.empty reg) main_clk) + p). +End RENUMBER. + Definition main_is_internal (p : RTL.program) : bool := let ge := Globalenvs.Genv.globalenv p in match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with |