From 6a204dda8e46d2d491de599c9c0dc6bceed5e971 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 3 May 2020 17:12:39 +0100
Subject: Add state transition conversion functions

---
 src/translation/Veriloggen.v | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index aa12a67..40876f7 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -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.
@@ -535,8 +547,8 @@ 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 :=
-- 
cgit