aboutsummaryrefslogtreecommitdiffstats
path: root/README.md
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-04-17 15:00:57 +0100
committerYann Herklotz <git@yannherklotz.com>2020-04-17 15:00:57 +0100
commit8de8b241d64a0fc7655609b0de426a32bd175f01 (patch)
tree16f86ae92ae2bcac4a036b4330c1f0908edb0aa6 /README.md
parentd1801b4b8f48791126b11ff7e10d98a4686527c3 (diff)
downloadvericert-8de8b241d64a0fc7655609b0de426a32bd175f01.tar.gz
vericert-8de8b241d64a0fc7655609b0de426a32bd175f01.zip
Add examples on how to run HLS tool
Diffstat (limited to 'README.md')
-rw-r--r--README.md10
1 files changed, 10 insertions, 0 deletions
diff --git a/README.md b/README.md
index de575c8..5c1d8a0 100644
--- a/README.md
+++ b/README.md
@@ -53,3 +53,13 @@ make install
```
Which will install the binary in `./bin/coqup` by default. However, this can be changed by changing the `PREFIX` environment variable, in which case the binary will be installed in `$PREFIX/bin/coqup`.
+
+## Running
+
+To test out `coqup` you can try the following examples which are in the test folder using the following:
+
+``` shell
+./bin/coqup test/loop.c -o loop.v
+./bin/coqup test/conditional.c -o conditional.v
+./bin/coqup test/add.c -o add.v
+```