From a72f26319dabca414a2b576424b9f72afaca161c Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Fri, 20 Nov 2020 21:32:21 +0000 Subject: Add wires and use them for output of instances [WIP] Add wires to HTL [WIP] Add wires to verilog [WIP] Use wire for finished signal [WIP] merge wire and scl [WIP] Fix wrong reg in ICall translation --- src/translation/HTLgen.v | 48 ++++++++++++++++++++++++++++++++++---------- src/translation/Veriloggen.v | 7 +++++-- 2 files changed, 42 insertions(+), 13 deletions(-) (limited to 'src/translation') diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index b6c4a25..be473fc 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -34,7 +34,7 @@ Record state: Type := mkstate { st_st : reg; st_freshreg: reg; st_freshstate: node; - st_scldecls: AssocMap.t (option io * scl_decl); + st_scldecls: AssocMap.t scl_decl; st_arrdecls: AssocMap.t (option io * arr_decl); st_insts: AssocMap.t instantiation; st_datapath: datapath; @@ -45,7 +45,7 @@ Definition init_state (st : reg) : state := mkstate st 1%positive 1%positive - (AssocMap.empty (option io * scl_decl)) + (AssocMap.empty scl_decl) (AssocMap.empty (option io * arr_decl)) (AssocMap.empty instantiation) (AssocMap.empty stmnt) @@ -140,7 +140,7 @@ Lemma declare_reg_state_incr : s.(st_st) s.(st_freshreg) s.(st_freshstate) - (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) + (AssocMap.set r (VScalar i sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_insts) s.(st_datapath) @@ -152,7 +152,7 @@ Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := s.(st_st) s.(st_freshreg) s.(st_freshstate) - (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) + (AssocMap.set r (VScalar i sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_insts) s.(st_datapath) @@ -274,7 +274,7 @@ Lemma add_instance_state_incr : Proof. Admitted. -Definition add_instance (mod_name: ident) (args: list reg) (rst: reg) (finished: reg) (dst: reg) : mon unit := +Definition add_instance (mod_name: ident) (args: list reg) (finished: reg) (dst: reg) : mon unit := fun s => let instname := assocmap_nextavailable s.(st_insts) in let inst := HTL.HTLinstantiation mod_name instname args dst finished in @@ -507,7 +507,7 @@ Lemma create_reg_state_incr: s.(st_st) (Pos.succ (st_freshreg s)) (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + (AssocMap.set s.(st_freshreg) (VScalar i sz) s.(st_scldecls)) s.(st_arrdecls) s.(st_insts) (st_datapath s) @@ -520,13 +520,39 @@ Definition create_reg (i : option io) (sz : nat) : mon reg := s.(st_st) (Pos.succ r) (st_freshstate s) - (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + (AssocMap.set s.(st_freshreg) (VScalar i sz) s.(st_scldecls)) (st_arrdecls s) (st_insts s) (st_datapath s) (st_controllogic s)) (create_reg_state_incr s sz i). +Lemma create_wire_state_incr: + forall s sz, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (VWire sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_insts) + (st_datapath s) + (st_controllogic s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_wire (sz : nat) : mon reg := + fun s => let r := s.(st_freshreg) in + OK r (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (VWire sz) s.(st_scldecls)) + (st_arrdecls s) + (st_insts s) + (st_datapath s) + (st_controllogic s)) + (create_wire_state_incr s sz). + Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := match ni with (n, i) => @@ -555,9 +581,9 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni | Icall sig (inl fn) args dst n' => error (Errors.msg "Indirect calls are not implemented.") | Icall sig (inr fn) args dst n' => if Z.leb (Z.pos n') Integers.Int.max_unsigned then - do rst <- create_reg None 1; - do finished <- create_reg None 1; - add_instance fn args rst finished dst + do finished <- create_wire 1; + do res <- create_wire 32; + add_instance fn args finished res 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.") @@ -678,7 +704,7 @@ Definition max_state (f: function) : state := mkstate st (Pos.succ st) (Pos.succ (max_pc_function f)) - (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st))) + (AssocMap.set st (VScalar None 32) (st_scldecls (init_state st))) (st_arrdecls (init_state st)) (st_insts (init_state st)) (st_datapath (init_state st)) diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index f9c88bf..07034cc 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -30,8 +30,11 @@ Definition transl_list_fun (a : node * Verilog.stmnt) := Definition transl_list st := map transl_list_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 * scl_decl) := + match a with + | (r, (VScalar io sz)) => (Vdecl io r sz) + | (r, VWire sz) => (Vdeclwire r sz) + end. Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl. -- cgit