aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/Verilog.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/verilog/Verilog.v')
-rw-r--r--src/verilog/Verilog.v5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 225d35d..09eb914 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -43,7 +43,10 @@ Definition posToValue (p : positive) : value :=
mkvalue size (Word.posToWord size p).
Definition intToValue (i : Integers.int) : value :=
- mkvalue 32%nat (Word.natToWord 32%nat (Z.to_nat (Integers.Int.unsigned i))).
+ mkvalue 32%nat (Word.ZToWord 32%nat (Integers.Int.unsigned i)).
+
+Definition valueToZ (v : value) : Z :=
+ Word.uwordToZ v.(vword).
Definition state : Type := PositiveMap.t value * PositiveMap.t value.