diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-08 23:34:15 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-08 23:34:15 +0100 |
| commit | 32990af23915c15e5cfd4cfe32c47cafa508f11d (patch) | |
| tree | d63e4df8e989c5fa51a3a240beca8e670d7a600a /src/verilog/Test.v | |
| parent | 32f0f542c18b73303613b53573e6c61bc7ae6890 (diff) | |
| download | vericert-32990af23915c15e5cfd4cfe32c47cafa508f11d.tar.gz vericert-32990af23915c15e5cfd4cfe32c47cafa508f11d.zip | |
Add AssocMap
Diffstat (limited to 'src/verilog/Test.v')
| -rw-r--r-- | src/verilog/Test.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/verilog/Test.v b/src/verilog/Test.v index f24612e..90c5312 100644 --- a/src/verilog/Test.v +++ b/src/verilog/Test.v @@ -88,10 +88,10 @@ Proof. trivial. Qed. Definition test_fextclk := initial_fextclk test_output_module. Lemma manual_simulation : - step (State test_output_module empty_assocset empty_assocset + step (State test_output_module empty_assocmap empty_assocmap test_fextclk 1 (32'h"1")) - (State test_output_module (add_assocset 7%positive (32'h"3") empty_assocset) - empty_assocset test_fextclk 2 (32'h"3")). + (State test_output_module (add_assocmap 7%positive (32'h"3") empty_assocmap) + empty_assocmap test_fextclk 2 (32'h"3")). Proof. repeat (econstructor; eauto); try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); |