From 2181eac18441168f773e3391c4671619f4339ee6 Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Mon, 25 Jan 2021 13:50:10 +0200 Subject: Implement renumbering (wrong) --- src/translation/Veriloggen.v | 276 ++++++++++++++++++++++++++++++++------ src/translation/Veriloggenproof.v | 7 +- 2 files changed, 243 insertions(+), 40 deletions(-) (limited to 'src/translation') diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index f9d4b64..6c472f5 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -17,60 +17,258 @@ *) From compcert Require Import Maps. -From compcert Require Errors. +From compcert Require Import Errors. From compcert Require Import AST. -From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt. +From vericert Require Import Vericertlib AssocMap ValueInt Statemonad. +From vericert Require Import HTL Verilog. -Definition transl_datapath_fun (a : node * HTL.datapath_stmnt) := +Record state: Type := mkstate { + st_freshreg : reg; + st_regmap : PTree.t reg; + }. + +Module VerilogState <: State. + Definition st := state. + + Definition st_prop (st1 st2 : state) := True. + + Lemma st_refl : forall (s : state), 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. constructor. Qed. +End VerilogState. +Export VerilogState. + +Module VerilogMonad := Statemonad(VerilogState). +Export VerilogMonad. + +Module VerilogMonadExtra := Monad.MonadExtra(VerilogMonad). +Import VerilogMonadExtra. +Export MonadNotation. + +Definition renumber_reg (r : reg) : mon reg := + do st <- get; + match PTree.get r st.(st_regmap) with + | Some reg' => ret reg' + | None => + do _ <- set (mkstate (Pos.succ st.(st_freshreg)) st.(st_regmap)) (fun _ => I); + ret st.(st_freshreg) + end. + +Definition transl_datapath_fun (a : Verilog.node * HTL.datapath_stmnt) := let (n, s) := a in - (Vlit (posToValue n), + (Verilog.Vlit (posToValue n), match s with - | HTLcall m args dst => Vskip - | HTLVstmnt s => s + | HTL.HTLcall m args dst => Verilog.Vskip (* inline_call m args *) + | HTL.HTLVstmnt s => s end). - Definition transl_datapath st := map transl_datapath_fun st. -Definition transl_ctrl_fun (a : node * Verilog.stmnt) := +Definition transl_ctrl_fun (a : Verilog.node * Verilog.stmnt) := let (n, stmnt) := a - in (Vlit (posToValue n), stmnt). + in (Verilog.Vlit (posToValue n), stmnt). Definition transl_ctrl st := map transl_ctrl_fun st. -Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) := - match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end. +Definition scl_to_Vdecl_fun (a : reg * (option Verilog.io * Verilog.scl_decl)) := + match a with (r, (io, Verilog.VScalar sz)) => (Verilog.Vdecl io r sz) end. Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl. -Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) := - match a with (r, (io, VArray sz l)) => (Vdeclarr io r sz l) end. +Definition arr_to_Vdeclarr_fun (a : reg * (option Verilog.io * Verilog.arr_decl)) := + match a with (r, (io, Verilog.VArray sz l)) => (Verilog.Vdeclarr io r sz l) end. Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. -Definition transl_module (m : HTL.module) : Verilog.module := - let case_el_ctrl := transl_ctrl (PTree.elements m.(mod_controllogic)) in - let case_el_data := transl_datapath (PTree.elements m.(mod_datapath)) in - let body := - Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1))) - (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint)))) - (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) - :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) - :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) - ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in - Verilog.mkmodule m.(mod_start) - m.(mod_reset) - m.(mod_clk) - m.(mod_finish) - m.(mod_return) - m.(mod_st) - m.(mod_stk) - m.(mod_stk_len) - m.(mod_params) - body - m.(mod_entrypoint). - -Definition transl_fundef := transf_fundef transl_module. - -Definition transl_program (p: HTL.program) : Verilog.program := - transform_program transl_fundef p. +Definition find_module (program : HTL.program) (name : ident) : mon HTL.module := + match option_map snd (find (fun named_module => Pos.eqb (fst named_module) name) program.(prog_defs)) with + | Some (Gfun (Internal f)) => ret f + | _ => error (Errors.msg "Veriloggen: Could not find definition for called module") + end. + +Fixpoint renumber_edge (edge : Verilog.edge) := + match edge with + | Vposedge r => + do r' <- renumber_reg r; + ret (Vposedge r') + | Vnegedge r => + do r' <- renumber_reg r; + ret (Vposedge r') + | Valledge => ret Valledge + | Voredge e1 e2 => + do e1' <- renumber_edge e1; + do e2' <- renumber_edge e2; + ret (Voredge e1' e2') + end. + +Definition renumber_declaration (decl : Verilog.declaration) := + match decl with + | Vdecl io reg sz => + do reg' <- renumber_reg reg; + ret (Vdecl io reg' sz) + | Vdeclarr io reg sz len => + do reg' <- renumber_reg reg; + ret (Vdeclarr io reg' sz len) + end. + + +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') + 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_item (item : Verilog.module_item) := + match item with + | Vdeclaration decl => + do decl' <- renumber_declaration decl; + ret (Vdeclaration decl') + | Valways edge stmnt => + do edge' <- renumber_edge edge; + do stmnt' <- renumber_stmnt stmnt; + ret (Valways edge' stmnt') + | Valways_ff edge stmnt => + do edge' <- renumber_edge edge; + do stmnt' <- renumber_stmnt stmnt; + ret (Valways edge' stmnt') + | Valways_comb edge stmnt => + do edge' <- renumber_edge edge; + do stmnt' <- renumber_stmnt stmnt; + ret (Valways edge' stmnt') + end. + + +Definition renumber_module (m : Verilog.module) : mon Verilog.module := + do mod_start' <- renumber_reg (Verilog.mod_start m); + do mod_reset' <- renumber_reg (Verilog.mod_reset m); + do mod_clk' <- renumber_reg (Verilog.mod_clk m); + do mod_finish' <- renumber_reg (Verilog.mod_finish m); + do mod_return' <- renumber_reg (Verilog.mod_return m); + do mod_st' <- renumber_reg (Verilog.mod_st m); + do mod_stk' <- renumber_reg (Verilog.mod_stk m); + do mod_args' <- traverselist renumber_reg (Verilog.mod_args m); + let mod_body' := (Verilog.mod_body m) in + + ret (Verilog.mkmodule + mod_start' + mod_reset' + mod_clk' + mod_finish' + mod_return' + mod_st' + mod_stk' + (Verilog.mod_stk_len m) + mod_args' + mod_body' + (Verilog.mod_entrypoint m)). + + +Definition called_functions : (list (Verilog.node * HTL.datapath_stmnt)) -> list ident := + flat_map (fun (a : (positive * HTL.datapath_stmnt)) => + let (n, stmt) := a in + match stmt with + | HTL.HTLcall fn _ _ => fn::nil + | _ => nil + end). + +(* FIXME Remove the fuel parameter (recursion limit)*) +Fixpoint transf_module (fuel : nat) (program : HTL.program) (m : HTL.module) : mon Verilog.module := + match fuel with + | O => error (Errors.msg "Veriloggen: transl_module ran out of fuel") + | S fuel' => + let case_el_ctrl := transl_ctrl (PTree.elements (HTL.mod_controllogic m)) in + let case_el_data := transl_datapath (PTree.elements (HTL.mod_datapath m)) in + + (* Inlining *) + let inline_names := called_functions (PTree.elements (HTL.mod_datapath m)) in + do inline_modules <- traverselist (find_module program) inline_names; + do translated_modules <- traverselist (transf_module fuel' program) inline_modules; + do renumbered_modules <- traverselist renumber_module translated_modules; + + let body := + Valways (Vposedge (HTL.mod_clk m)) (Vcond (Vbinop Veq (Vvar (HTL.mod_reset m)) (Vlit (ZToValue 1))) + (Vnonblock (Vvar (HTL.mod_st m)) (Vlit (posToValue (HTL.mod_entrypoint m)))) + (Vcase (Vvar (HTL.mod_st m)) case_el_ctrl (Some Vskip))) + :: Valways (Vposedge (HTL.mod_clk m)) (Vcase (Vvar (HTL.mod_st m)) case_el_data (Some Vskip)) + :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements (HTL.mod_arrdecls m)) + ++ scl_to_Vdecl (AssocMap.elements (HTL.mod_scldecls m))) + ++ List.flat_map (fun m => (Verilog.mod_body m)) renumbered_modules in + + ret (Verilog.mkmodule + (HTL.mod_start m) + (HTL.mod_reset m) + (HTL.mod_clk m) + (HTL.mod_finish m) + (HTL.mod_return m) + (HTL.mod_st m) + (HTL.mod_stk m) + (HTL.mod_stk_len m) + (HTL.mod_params m) + body + (HTL.mod_entrypoint m) + ) + end. + +Definition transl_module (prog : HTL.program) (m : HTL.module) := + run_mon (mkstate xH (PTree.empty reg)) (transf_module 10 prog m). + +Definition transl_fundef (prog : HTL.program) := transf_partial_fundef (transl_module prog). +Definition transl_program (prog : HTL.program) := transform_partial_program (transl_fundef prog) prog. diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index c83a3b1..59267f7 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -17,14 +17,18 @@ *) From compcert Require Import Smallstep Linking Integers Globalenvs. +From compcert Require Errors. From vericert Require HTL. From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap. Require Import Lia. + Local Open Scope assocmap. Definition match_prog (prog : HTL.program) (tprog : Verilog.program) := - match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog. + match_program (fun cu f tf => Errors.OK tf = transl_fundef prog f) eq prog tprog. + +(* Lemma transf_program_match: forall prog, match_prog prog (transl_program prog). @@ -404,3 +408,4 @@ Section CORRECTNESS. Qed. End CORRECTNESS. +*) -- cgit