From 78e549331ba3f136ebe94955f68767bd384df454 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 6 Jul 2020 14:09:54 +0100 Subject: HTLgenproof compiles again - Commented out Iload, Istore proofs for now --- src/verilog/HTL.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/verilog/HTL.v') diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 3ba5b59..b3d1442 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -141,8 +141,10 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := forall g m args res, step g (Callstate res m args) Events.E0 (State res m m.(mod_entrypoint) - (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) - (init_regs args m.(mod_params))) + (AssocMap.set (mod_reset m) (ZToValue 0) + (AssocMap.set (mod_finish m) (ZToValue 0) + (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) + (init_regs args m.(mod_params))))) (empty_stack m)) | step_return : forall g m asr asa i r sf pc mst, -- cgit