diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-04-24 22:16:01 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-04-24 22:16:01 +0100 |
| commit | 57d74093a19569b9dd55520c6a1548e4827f3b1e (patch) | |
| tree | 62daff6f1d71b5d44ddb57b2c1429fac99267ecf | |
| parent | 6557bd4ad48626d1c7f644f4134560d363786766 (diff) | |
| download | vericert-57d74093a19569b9dd55520c6a1548e4827f3b1e.tar.gz vericert-57d74093a19569b9dd55520c6a1548e4827f3b1e.zip | |
Add valueToInt function
| -rw-r--r-- | src/verilog/Value.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index fe53dbc..241534c 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -78,6 +78,9 @@ Definition uvalueToZ (v : value) : Z := Definition intToValue (i : Integers.int) : value := ZToValue Int.wordsize (Int.unsigned i). +Definition valueToInt (i : value) : Integers.int := + Int.repr (valueToZ i). + (** Convert a [value] to a [bool], so that choices can be made based on the result. This is also because comparison operators will give back [value] instead of [bool], so if they are in a condition, they will have to be converted before |