diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-05-07 17:21:51 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-07 17:21:51 +0100 |
commit | c8535e1f454c7014c7b794fc8be343e2fda97937 (patch) | |
tree | 87d9d3fdba98457ba70d7756cc6a1e19e185ff69 /src/verilog/Test.v | |
parent | 1d6589fbda24fb57c9ab74d4bd41fa1a487a2c62 (diff) | |
download | vericert-kvx-c8535e1f454c7014c7b794fc8be343e2fda97937.tar.gz vericert-kvx-c8535e1f454c7014c7b794fc8be343e2fda97937.zip |
Rename assoclist to assocset
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 5cd6ec4..f24612e 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_assoclist empty_assoclist + step (State test_output_module empty_assocset empty_assocset test_fextclk 1 (32'h"1")) - (State test_output_module (add_assoclist 7%positive (32'h"3") empty_assoclist) - empty_assoclist test_fextclk 2 (32'h"3")). + (State test_output_module (add_assocset 7%positive (32'h"3") empty_assocset) + empty_assocset test_fextclk 2 (32'h"3")). Proof. repeat (econstructor; eauto); try (unfold ZToValue; instantiate (1 := eq_refl (vsize (1'h"1"))); auto); |