From 044a68b1b215125e2651c637f28c794536d27ba5 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Sun, 14 Jun 2020 16:41:27 +0100 Subject: Array semantics now uses dependent Array type. --- src/translation/Veriloggen.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/translation/Veriloggen.v') diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index efe3565..2b9974b 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -29,13 +29,13 @@ Fixpoint transl_list (st : list (node * Verilog.stmnt)) {struct st} : list (expr Fixpoint scl_to_Vdecl (scldecl : list (reg * (option io * scl_decl))) {struct scldecl} : list module_item := match scldecl with - | (r, (io, Scalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl' + | (r, (io, VScalar sz))::scldecl' => Vdeclaration (Vdecl io r sz) :: scl_to_Vdecl scldecl' | nil => nil end. Fixpoint arr_to_Vdeclarr (arrdecl : list (reg * (option io * arr_decl))) {struct arrdecl} : list module_item := match arrdecl with - | (r, (io, Array sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl' + | (r, (io, VArray sz l))::arrdecl' => Vdeclaration (Vdeclarr io r sz l) :: arr_to_Vdeclarr arrdecl' | nil => nil end. @@ -56,6 +56,7 @@ Definition transl_module (m : HTL.module) : Verilog.module := m.(mod_return) m.(mod_st) m.(mod_stk) + m.(mod_stk_len) m.(mod_params) body m.(mod_entrypoint). -- cgit