initial import from 893d804da923125e7977c58646f1cce613d06583

.gitignore

@@ -0,0 +1,26 @@
+*.annot
+*.cmo
+*.cma
+*.cmi
+*.a
+*.o
+*.cmx
+*.cmxs
+*.cmxa
+
+# ocamlbuild working directory
+_build/
+
+# ocamlbuild targets
+*.byte
+*.native
+
+# oasis generated files
+setup.data
+setup.log
+
+# Merlin configuring file for Vim and Emacs
+.merlin
+
+.DS_Store
+memo.md

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2018 Preferred Networks, Inc.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

Makefile

@@ -0,0 +1,5 @@
+build:
+	dune build src/main.exe
+
+clean:
+	dune clean

README-ja.md

@@ -0,0 +1,89 @@
+# SystemVerilog 用の自動テストケース生成ツール
+
+SystemVerilog を対象に Concolic Testing を行うプロトタイプです。
+シミュレータによる実行と、シンボリック実行を交互に繰り返すことで SystemVerilog で記述された回路に対するラインカバレッジ100%のテストケースを生成します（DART[1]やHYBRO[2]などと同様）。
+
+現状では、サポートしている SystemVerilog の機能と性能に制限があります。
+
+**Disclaimer: PFN provides no warranty or support for this software. Use it at your own risk.**
+
+このソフトウェアは[PFN2018 夏季インターン](https://www.preferred-networks.jp/ja/news/internship2018summer_jp)の一環として、主に押川広樹さんによって開発されました。
+
+## 実行方法
+
+### 依存
+
+* OCaml (>= 4.05.0)
+  * dune (>= 1.0.1)
+  * z3 (>= 4.7.1)
+  * ocamlgraph (>= 1.8.8)
+  * ppx_deriving (>= 4.2.1)
+* [Z3](https://github.com/Z3Prover/z3) (>= 4.7.1)
+* [menhir](http://gallium.inria.fr/~fpottier/menhir/) (>= 20180703)
+* SystemVerilog Simulator
+
+OCamlの ライブラリと menhir は [opam](https://opam.ocaml.org/) からインストール出来ます。
+
+### ビルド & 実行
+
+```sh
+make
+_build/default/src/main.exe -i file.sv -f file.bin -v log.vcd -s script.sh
+```
+
+現状では、パーサの warning が大量に出ます。
+
+* `file.sv` : 対象の SystemVerilog プログラム
+* `file.bin` : 実行中に回路の入力ベクトルを読み書きするためのファイル
+* `log.vcd` : シミュレーション結果が出力される VCD ファイル
+* `script.sh` : シミュレーションを実行するシェルスクリプト。`file.sv` の回路を `file.bin` の入力に対して実行し、結果を `log.vcd` として出力することが必要。
+
+#### オプション
+
+```txt
+-c              dump coverage information
+-dparse         dump parsed tree
+-dir            dump IR
+-dcfg           generate dot files from CFG
+-dtrace         dump trace
+-dz3            dump z3 log
+-dinputs file   dump all input vectors to [file]
+-test           run without concrete execution
+```
+
+## 動作原理
+
+1. ソースコードを解析して Control Flow Graph(CFG) を生成
+2. シミュレーションのためにランダムな入力ベクトルを生成
+3. シミュレーションを実行
+4. VCD を元に CFG のどのパスが実行されたかを計算
+5. 実行されていない部分を実行するのに必要な制約をシンボリックに求める
+6. SMT ソルバーを用いて制約を解く
+7. 得られた解から入力に関わる部分を取り出して、次の入力とする
+8. 全ての部分が実行されるまで 3-7 を繰り返す
+
+上の過程で得られた入力ベクトルがテストケースとなる。
+
+![overview](overview.svg)
+
+## src/ のファイル構成
+
+* lexer.mll:     レキサー
+* parser.mly:    パーサー
+* parsetree.ml:  パース後の抽象構文木
+* ir.ml:         簡潔な内部表現と抽象構文木からの変換
+* cfg.ml:        CFG と 内部表現からの変換
+* vis.ml:        CFG の可視化のための関数
+* ce.ml:         VCD と CFG から実行されたパスを計算
+* constraint.ml: まだカバーされていない CFG のパスをたどるために必要な制約を計算
+* solve.ml:      Z3 を用いて制約を解消
+* main.ml:       全体をくっつける
+
+## ライセンス
+
+MITライセンス（詳細は [LICENSE](./LICENSE) ファイルを参照）。
+
+## 参考文献
+
+* [1] P. Godefroid, N. Klarlund, and K. Sen, DART: Directed Automated Random Testing. In Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation (PLDI'05), 2005.
+* [2] L. Liu and S. Vasudevan, Efficient validation input generation in RTL by hybridized source code analysis, In Proceedings of the 2011 Design, Automation & Test in Europe, Grenoble, 2011.

README.md

@@ -0,0 +1,89 @@
+# Automatic Test Generator for SystemVerilog
+
+This is a prototype of Concolic Testing engine for SystemVerilog.
+This program generates 100% line-of-code coverage test cases for a circuit written in SystemVerilog by alternatively repeating concrete execution and simbolic execution in the similar way as DART[1] and HYBRO[2].
+
+There are several limitations on supported SystemVerilog Features.
+
+**Disclaimer: PFN provides no warranty or support for this software. Use it at your own risk.**
+
+This software is developed as part of [PFN summer internship 2018](https://www.preferred-networks.jp/en/news/internship2018summer) and the main developer is Hiroki Oshikawa.
+
+## How to use
+
+### Dependencies
+
+* OCaml (>= 4.05.0)
+  * dune (>= 1.0.1)
+  * z3 (>= 4.7.1)
+  * ocamlgraph (>= 1.8.8)
+  * ppx_deriving (>= 4.2.1)
+* [Z3](https://github.com/Z3Prover/z3) (>= 4.7.1)
+* [menhir](http://gallium.inria.fr/~fpottier/menhir/) (>= 20180703)
+* SystemVerilog Simulator
+
+OCaml libraries and menhir can be installed through [opam](https://opam.ocaml.org/).
+
+### Build and Run
+
+```sh
+make
+_build/default/src/main.exe -i file.sv -f file.bin -v log.vcd -s script.sh
+```
+
+Note: `make` emits many warnings for now.
+
+* `file.sv` : Target program written in SystemVerilog
+* `file.bin` : File used to read and write input vectors during execution
+* `log.vcd` : VCD file
+* `script.sh` : Shell script to run a simulator. It is assumed that `file.sh` runs `file.sv` against input vectors in `file.bin` and dump a result into `log.vcd`.
+
+#### Options
+
+```txt
+-c              dump coverage information
+-dparse         dump parsed tree
+-dir            dump IR
+-dcfg           generate dot files from CFG
+-dtrace         dump trace
+-dz3            dump z3 log
+-dinputs file   dump all input vectors to [file]
+-test           run without concrete execution
+```
+
+## Procedure of test case generation
+
+1. Parse a program source code and generate Control Flow Graphs (CFG)
+2. Generate input vectors randomly
+3. Run simulator
+4. Calculate which paths in CFGs were executed from the dumped VCD file
+5. Generate constraints symbolically to execute a part of the program that has not been executed yet
+6. Solve the constraints using SMT
+7. Extract next input vectors from the solution
+8. Repeat 3-7 until all parts of the program are executed
+
+Input vectors generated above procedure comprise a test case.
+
+![overview](overview.svg)
+
+## Structure of `src/`
+
+* lexer.mll:     Lexer
+* parser.mly:    Parser
+* parsetree.ml:  Abstract syntax tree
+* ir.ml:         Simple intermediate representation(IR) and translation from AST
+* cfg.ml:        CFG and translation from IR
+* vis.ml:        Visualization of CFG
+* ce.ml:         Calculate executed paths from VCD and CFG
+* constraint.ml: Calculate constraints
+* solve.ml:      Solve the constraints using Z3
+* main.ml:       Put together above
+
+## License
+
+MIT License (see the [LICENSE](./LICENSE) file for details).
+
+## References
+
+* [1] P. Godefroid, N. Klarlund, and K. Sen, DART: Directed Automated Random Testing. In Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation (PLDI'05), 2005.
+* [2] L. Liu and S. Vasudevan, Efficient validation input generation in RTL by hybridized source code analysis, In Proceedings of the 2011 Design, Automation & Test in Europe, Grenoble, 2011.

dune-project

@@ -0,0 +1,2 @@
+(lang dune 1.0)
+(using menhir 1.0)

examples/.gitignore

@@ -0,0 +1,4 @@
+tmp*
+*.log
+*.ast
+*.txt

preprocessor/define.py

@@ -0,0 +1,67 @@
+#!/usr/local/bin/python3
+
+import sys
+import os
+import glob
+import shutil
+
+def make_db(filename):
+    db = {}
+    with open(filename) as f:
+        for line in f:
+            l = line.strip().split()
+            if len(l) > 0 and l[0] == "`define":
+                db["`" + l[1]] = l[2]
+    return db
+
+def translate(st, db):
+    for s, t in db.items():
+        st = st.replace(s, t)
+    return st
+
+def replace(filename, db):
+    res = []
+    with open(filename) as f:
+        for line in f:
+            tmp = translate(line, db)
+            ll = line.split()
+            if len(ll) > 0 and ll[0] == "`define":
+                tmp = ""
+            res.append(tmp)
+    return res
+
+def mk_new_filename(filename):
+    l = filename.split("/")
+    fn = l[-1]
+    nf = fn.split(".")[0] + "_pp.sv"
+    ll = l[0:-1] + [nf]
+    return "/".join(ll)
+
+def rewrite(filename, data):
+    new_filename = mk_new_filename(filename)
+    with open(new_filename, "w") as f:
+        f.writelines(data)
+
+def move_pp(dirname):
+    new_dir = dirname + "pp/"
+    os.mkdir(new_dir)
+    pp_sv_files = glob.glob(dirname + "*_pp.sv")
+    for f in pp_sv_files:
+        shutil.move(f, new_dir)
+
+
+
+
+if __name__ == '__main__':
+    dirname = sys.argv[1]
+    sv_files = glob.glob(dirname + "*.sv")
+    db = {}
+    for svf in sv_files:
+        ndb = make_db(svf)
+        db = {**db, **ndb}
+    for svf in sv_files:
+        res = replace(svf, db)
+        rewrite(svf, res)
+    move_pp(dirname)
+
+

src/.gitignore

@@ -0,0 +1,5 @@
+memo.md
+*.sv
+tmp*
+*.log
+parser.txt

src/Makefile

@@ -0,0 +1,2 @@
+sim_add_pure:
+	@echo "simulating..."