diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-05-03 17:12:39 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-03 17:12:39 +0100 |
commit | 6a204dda8e46d2d491de599c9c0dc6bceed5e971 (patch) | |
tree | 6241e4e6b98922b74dd53ceba503164a9c338a3e /src/translation | |
parent | 7ee0ca8263632536582646eb83b909f78f9e6fe4 (diff) | |
download | vericert-6a204dda8e46d2d491de599c9c0dc6bceed5e971.tar.gz vericert-6a204dda8e46d2d491de599c9c0dc6bceed5e971.zip |
Add state transition conversion functions
Diffstat (limited to 'src/translation')
-rw-r--r-- | src/translation/Veriloggen.v | 16 |
1 files 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 := |