aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorNadesh Ramanathan <nadeshramanathan88@gmail.com>2020-06-27 14:02:42 +0100
committerNadesh Ramanathan <nadeshramanathan88@gmail.com>2020-06-27 14:02:42 +0100
commite5cbd4cc39d406110e61de530987603a3634d43a (patch)
tree99e6c84d54f631bdd77847373432411344938259
parent1781898f024b71106ee3d074fe03c830356ec580 (diff)
parentcc4f6d5ff88a40eb5c5f3f13d8b1d8022e8161ba (diff)
downloadvericert-kvx-dev-initial.tar.gz
vericert-kvx-dev-initial.zip
Merge branch 'dev-initial' of https://github.com/ymherklotz/coqup into dev-initialdev-initial
-rw-r--r--src/translation/Veriloggen.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 48ee997..fa57f2e 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -50,14 +50,14 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in
let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in
let body :=
- (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) ++
+ arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) ++
+ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls)) ++
(Vinitial (stackinit_to_Vinitial m.(mod_stk) (PTree.elements m.(mod_stackinit)))
:: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
:: Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (ZToValue 1 1))
(Vnonblock (Vvar m.(mod_st)) (posToValue 32 m.(mod_entrypoint)))
(Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
- :: nil)
- ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
+ :: nil) in
Verilog.mkmodule m.(mod_start)
m.(mod_reset)
m.(mod_clk)