Merge pull request #1700 from GaloisInc/sb/yosys

Add commands for analysis of VHDL via Yosys
GaloisInc · Oct 7, 2022 · 2c5cffd · 2c5cffd
2 parents cd3f141 + 2664d83
commit 2c5cffd
Show file tree

Hide file tree

Showing 53 changed files with 6,010 additions and 40 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -43,3 +43,6 @@
 [submodule "deps/language-rust"]
 	path = deps/language-rust
 	url = https://github.com/harpocrates/language-rust.git
+[submodule "deps/language-sally"]
+	path = deps/language-sally
+	url = https://github.com/GaloisInc/language-sally
diff --git a/cabal.project b/cabal.project
@@ -17,6 +17,8 @@ packages:
     deps/aig
     deps/cryptol
     deps/what4/what4
+    deps/what4/what4-transition-system
+    deps/language-sally
     deps/crucible/crucible
     deps/crucible/crucible-concurrency
     deps/crucible/crucible-jvm

diff --git a/deps/language-sally b/deps/language-sally
diff --git a/deps/what4 b/deps/what4
+4 −1		.github/workflows/gen_matrix.pl
+3 −1		.github/workflows/test.yml
+5 −5		README.md
+43 −34		what4-transition-system/src/What4/TransitionSystem.hs
+5 −0		what4/CHANGES.md
+1 −1		what4/LICENSE
+1 −0		what4/README.md
+1 −1		what4/doc/implementation.md
+1 −1		what4/src/What4/Expr/AppTheory.hs
+3 −3		what4/src/What4/ProblemFeatures.hs
+2 −2		what4/src/What4/Protocol/SMTLib2.hs
+7 −1		what4/src/What4/Protocol/SMTLib2/Syntax.hs
+12 −0		what4/src/What4/Solver.hs
+3 −2		what4/src/What4/Solver/Boolector.hs
+4 −4		what4/src/What4/Solver/CVC4.hs
+240 −0		what4/src/What4/Solver/CVC5.hs
+1 −0		what4/test/AdapterTest.hs
+3 −1		what4/test/ExprBuilderSMTLib2.hs
+5 −2		what4/test/OnlineSolverTest.hs
+4 −3		what4/test/TestTemplate.hs
+3 −2		what4/what4.cabal