diff options
author | James Pollard <james@pollard.dev> | 2020-06-14 16:41:27 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-14 16:41:27 +0100 |
commit | 044a68b1b215125e2651c637f28c794536d27ba5 (patch) | |
tree | 53c0a4c94b048fa1f96d7cdf3ef73169b6fe2398 /src/translation/Veriloggen.v | |
parent | 39d438f9c2b3d1484ae0e2afe33a19c2f654a8b0 (diff) | |
download | vericert-044a68b1b215125e2651c637f28c794536d27ba5.tar.gz vericert-044a68b1b215125e2651c637f28c794536d27ba5.zip |
Array semantics now uses dependent Array type.
Diffstat (limited to 'src/translation/Veriloggen.v')
-rw-r--r-- | src/translation/Veriloggen.v | 5 |
1 files changed, 3 insertions, 2 deletions
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). |