diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-11-17 13:14:56 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-11-17 13:14:56 +0000 |
| commit | 2a5b73153060ff9f69403ca81d29c9c9761623d8 (patch) | |
| tree | 089028e9186eb3dc8f2d38f580832d911a807597 /src/hls/Veriloggen.v | |
| parent | 7d9057a6ca6f591851ee5c6e8d74e3833aae3903 (diff) | |
| download | vericert-kvx-2a5b73153060ff9f69403ca81d29c9c9761623d8.tar.gz vericert-kvx-2a5b73153060ff9f69403ca81d29c9c9761623d8.zip | |
Add changes for proof of reset signals with Resetstate
Diffstat (limited to 'src/hls/Veriloggen.v')
| -rw-r--r-- | src/hls/Veriloggen.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index a0be0fa..b497115 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -44,7 +44,9 @@ Definition transl_module (m : HTL.module) : Verilog.module := Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1))) (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint)))) (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) - :: 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)) (Vlit (ZToValue 0))) + (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) + Vskip) :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in Verilog.mkmodule m.(mod_start) |