diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-04-22 00:13:04 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-04-22 00:13:04 +0100 |
| commit | b9785cabf40b9b7708f1c0d5a622d7fc4713c38d (patch) | |
| tree | 8fc468709007aa27aa3a6d7f8305b2ad6ea37d13 /src/Simulator.v | |
| parent | 83998e544f51f06026fb32d115b74f9d1303e629 (diff) | |
| download | vericert-b9785cabf40b9b7708f1c0d5a622d7fc4713c38d.tar.gz vericert-b9785cabf40b9b7708f1c0d5a622d7fc4713c38d.zip | |
Return the actual result of the module
Diffstat (limited to 'src/Simulator.v')
| -rw-r--r-- | src/Simulator.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/Simulator.v b/src/Simulator.v index 3c5aca0..6849f80 100644 --- a/src/Simulator.v +++ b/src/Simulator.v @@ -25,8 +25,11 @@ From coqup Require Import Coquplib. Local Open Scope error_monad_scope. -Definition simulate (n : nat) (m : Verilog.module) : res (list (positive * Value.value)) := +Definition simulate (n : nat) (m : Verilog.module) : res (Value.value * list (positive * Value.value)) := do map <- Verilog.module_run n m; - OK (PositiveMap.elements map). + match PositiveMap.find (fst (Verilog.mod_return m)) map with + | Some v => OK (v, (PositiveMap.elements map)) + | None => Error (msg "Could not find result.") + end. Local Close Scope error_monad_scope. |