diff options
author | James Pollard <james@pollard.dev> | 2020-05-30 18:38:50 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-05-30 18:38:50 +0100 |
commit | c3fe9469171bbf706dcb7bc84297123590377100 (patch) | |
tree | bfaa79704f70eb0c896d598ae2abc5235db56211 /src/translation/Veriloggen.v | |
parent | 6059f00139e2ce90525a1e1023ca97b6ba65e6bb (diff) | |
parent | acf638b44023c5593e0758e82d161c087062dc39 (diff) | |
download | vericert-c3fe9469171bbf706dcb7bc84297123590377100.tar.gz vericert-c3fe9469171bbf706dcb7bc84297123590377100.zip |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/translation/Veriloggen.v')
-rw-r--r-- | src/translation/Veriloggen.v | 71 |
1 files changed, 51 insertions, 20 deletions
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index 412dc28..4a6f23e 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -1,4 +1,4 @@ -(* -*- mode: coq -*- +(* * CoqUp: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * @@ -38,6 +38,18 @@ Inductive statetrans : Type := | StateGoto (p : node) | StateCond (c : expr) (t f : node). +Definition state_goto (st : reg) (n : node) : stmnt := + Vnonblock (Vvar st) (Vlit (posToValue 32 n)). + +Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := + Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)). + +Definition statetrans_transl (stvar : reg) (st : statetrans) : stmnt := + match st with + | StateGoto p => state_goto stvar p + | StateCond c t f => state_cond stvar c t f + end. + Definition valid_freshstate (stm: PositiveMap.t stmnt) (fs: node) := forall (n: node), Plt n fs \/ stm!n = None. @@ -371,6 +383,10 @@ Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := | _, _, _ => Error (Errors.msg "Veriloggen.add_instr") end. +(** Add a register to the state without changing the [st_freshreg], as this +should already be the right value. This can be assumed because the max register +is taken from the RTL code. *) + Definition add_reg (r: reg) (s: state) : state := mkstate (st_freshreg s) (st_freshstate s) @@ -410,6 +426,9 @@ Lemma decl_io_state_incr: (st_wf s)). Proof. constructor; simpl; auto using Ple_succ with verilog_state. Qed. +(** Declare a new register by incrementing the [st_freshreg] by one and +returning the old [st_freshreg]. *) + Definition decl_io (d: decl) : mon (reg * decl) := fun s => let r := s.(st_freshreg) in OK (r, d) (mkstate @@ -421,6 +440,9 @@ Definition decl_io (d: decl) : mon (reg * decl) := (st_wf s)) (decl_io_state_incr s). +(** Declare a new register which is given, by changing [st_decl] and without +affecting anything else. *) + Definition declare_reg (r: reg) (d: decl): mon (reg * decl) := fun s => OK (r, d) (mkstate (st_freshreg s) @@ -431,6 +453,9 @@ Definition declare_reg (r: reg) (d: decl): mon (reg * decl) := (st_wf s)) (change_decl_state_incr s (PositiveMap.add r d s.(st_decl))). +(** Declare a new fresh register by first getting a valid register to increment, +and then adding it to the declaration list. *) + Definition decl_fresh_reg (d: decl) : mon (reg * decl) := do (r, d) <- decl_io d; declare_reg r d. @@ -557,18 +582,17 @@ Definition make_stm (r : reg) (s : PositiveMap.t stmnt) : stmnt := Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr * stmnt := match st with - | (n, StateGoto n') => (posToExpr 32 n, nonblock r (posToExpr 32 n')) - | (n, StateCond c n1 n2) => (posToExpr 32 n, nonblock r (Vternary c (posToExpr 32 n1) (posToExpr 32 n2))) + | (n, StateGoto n') => (posToExpr 32 n, state_goto r n') + | (n, StateCond c n1 n2) => (posToExpr 32 n, state_cond r c n1 n2) end. Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt := Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)) (Some Vskip). -Fixpoint allocate_regs (e : list (reg * decl)) {struct e} : list module_item := +Definition allocate_reg (e : reg * decl) : module_item := match e with - | (r, (mkdecl n 0))::es => Vdecl r n :: allocate_regs es - | (r, (mkdecl n l))::es => Vdeclarr r n l :: allocate_regs es - | nil => nil + | (r, (mkdecl n 0)) => Vdecl r n + | (r, (mkdecl n l)) => Vdeclarr r n l end. Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list module_item := @@ -577,7 +601,7 @@ Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list m (nonblock st (posToExpr 32 entry)) (make_statetrans st s.(st_statetrans)))) :: (Valways_ff (Vposedge clk) (make_stm st s.(st_stm))) - :: (allocate_regs (PositiveMap.elements s.(st_decl))). + :: (map allocate_reg (PositiveMap.elements s.(st_decl))). (** To start out with, the assumption is made that there is only one function/module in the original code. *) @@ -598,20 +622,9 @@ Definition transf_module (f: function) : mon module := do st <- decl_fresh_reg (mkdecl 32 0); do current_state <- get; let mi := make_module_items f.(fn_entrypoint) (fst clk) (fst st) (fst rst) current_state in - ret (mkmodule (get_sz start) (get_sz rst) (get_sz clk) (get_sz fin) (get_sz rtrn) + ret (mkmodule (get_sz start) (get_sz rst) (get_sz clk) (get_sz fin) (get_sz rtrn) (get_sz st) (map set_int_size f.(fn_params)) mi). -Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit)) -{struct flist} : option function := - match flist with - | (i, AST.Gfun (AST.Internal f)) :: xs => - if Pos.eqb i main - then Some f - else main_function main xs - | _ :: xs => main_function main xs - | nil => None - end. - Lemma max_state_valid_freshstate: forall f, valid_freshstate (st_stm init_state) (Pos.succ (max_pc_function f)). @@ -632,6 +645,24 @@ Definition max_state (f: function) : state := (st_decl init_state) (max_state_st_wf f). +Definition transl_module (f : function) : Errors.res module := + run_mon (max_state f) (transf_module f). + +(** Retrieve the main function from the RTL, this should probably be replaced by +retrieving a designated function instead. This could be passed on the +commandline and be assumed as a [Parameter] in this code. *) + +Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit)) +{struct flist} : option function := + match flist with + | (i, AST.Gfun (AST.Internal f)) :: xs => + if Pos.eqb i main + then Some f + else main_function main xs + | _ :: xs => main_function main xs + | nil => None + end. + Definition transf_program (d : program) : Errors.res module := match main_function d.(AST.prog_main) d.(AST.prog_defs) with | Some f => run_mon (max_state f) (transf_module f) |