aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-02-04 15:35:16 +0000
committerYann Herklotz <git@yannherklotz.com>2020-02-04 15:35:16 +0000
commit661484424bbb1bc55604ee1448012ca10c4b8804 (patch)
treeb0c13d9f07b7798beb6ee52da3703c7ba8b4ebe4
parent9042f09ecc607bb42de5d04ce6598c44991cef4c (diff)
downloadvericert-661484424bbb1bc55604ee1448012ca10c4b8804.tar.gz
vericert-661484424bbb1bc55604ee1448012ca10c4b8804.zip
Add extraction
-rw-r--r--extraction/Extraction.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/extraction/Extraction.v b/extraction/Extraction.v
new file mode 100644
index 0000000..40bbe54
--- /dev/null
+++ b/extraction/Extraction.v
@@ -0,0 +1,4 @@
+Require Import Verilog.
+
+Cd "src".
+Separate Extraction Verilog.nat_to_value Verilog.value_to_nat.