Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add commands for analysis of VHDL via Yosys #1700

Merged
merged 51 commits into from
Oct 7, 2022
Merged

Add commands for analysis of VHDL via Yosys #1700

Show file tree
Hide file tree
Changes from 50 commits
Commits
Show all changes
51 commits
Select commit Hold shift + click to select a range
43c85cb
Initial support for converting Yosys IR to SAWCore
chameco Nov 21, 2021
f694ece
Split and join terms that don't line up exactly
chameco Jan 3, 2022
31954a5
Build TypedTerms correctly, put extracted terms inside functions
chameco Jan 3, 2022
702a4f6
Remove unnecessary import
chameco Jan 3, 2022
28d10fa
Support for user-defined cells
chameco Jan 23, 2022
4f9aacf
Use Cryptol record encoding
chameco Feb 1, 2022
9f2df28
Implement some more cell types
chameco Feb 10, 2022
da97203
Improved interface; now Yosys files are imported as records
chameco Feb 11, 2022
98c6027
Tentative steps toward compositional reasoning
chameco Feb 14, 2022
fb9b753
Update manual.md
chameco Feb 23, 2022
cd4571b
Interface changes for yosys_verify
chameco Feb 23, 2022
08bd920
Update manual.md
chameco Feb 23, 2022
0bc2453
Update manual.md
chameco Feb 23, 2022
bc031f2
Tentative saw-remote-api updates
chameco Mar 1, 2022
2ee4444
Update saw-remote-api
chameco Mar 10, 2022
e51d21f
Preliminary translation of sequential circuits
chameco Apr 3, 2022
82061e0
Refactoring to support better sequential circuit translation
chameco May 1, 2022
ea9fd93
Fix $mux cell
chameco May 16, 2022
7adde62
Extraction of non-stateful terms given a finite number of iterations
chameco May 19, 2022
9632565
Use cell names for DFF state lookups instead of a placeholder
chameco May 21, 2022
c44bb9c
Fixes for shifts and arithmetic cells, improved sequential circuits
chameco May 23, 2022
e696ba6
Remove debug print statement
chameco May 31, 2022
0f41b6f
Add preliminary support for model checker query
chameco Jun 6, 2022
21013de
Better model checker export, Python stuff
chameco Jun 13, 2022
42aa4de
Add some documentation
chameco Jul 1, 2022
f96f9b8
Update what4 commit
Jul 7, 2022
b103d83
Fix warnings
chameco Jul 25, 2022
883950d
Better exception handling, add nonces to Yosys-derived names
chameco Sep 18, 2022
83f9eb7
Add CPP to handle containers on GHC 8.8
chameco Sep 18, 2022
d829e1f
Replace another reverseTopSort
chameco Sep 18, 2022
ba181c5
Merge branch 'master' into sb/yosys
chameco Sep 18, 2022
8389a79
Refactor to support recent changes to TopLevel
chameco Sep 18, 2022
d701156
Update saw-remote-api docs
chameco Sep 19, 2022
a434e36
Add a number of integration tests
chameco Sep 19, 2022
d4adc75
Extend / truncate terms
chameco Sep 24, 2022
1f9d8d6
Use some more structured exceptions
chameco Sep 24, 2022
3077af3
Fix incorrect vector SAWCore type
chameco Sep 25, 2022
b57d1ae
Typecheck intermediate SAWCore terms
chameco Sep 25, 2022
6ef682d
Typecheck some additional intermediate SAWCore terms
chameco Sep 25, 2022
3e3c20d
Fix warning
chameco Sep 25, 2022
958e2d8
Support implicit Yosys extensions and truncations
chameco Sep 26, 2022
52787e1
Add zenc dependency
chameco Sep 26, 2022
644a604
Ensure that state field names are valid Cryptol identifiers
chameco Sep 26, 2022
9993b43
Add yosys_extract_sequential_with_state
chameco Sep 26, 2022
168fd86
Merge branch 'master' into sb/yosys
chameco Sep 26, 2022
d093dee
Revert change to s2nTests/docker/saw.dockerfile
chameco Sep 26, 2022
1a76325
More aggressively check combinational terms, fix bit outputs
chameco Sep 28, 2022
caffef4
Add Haddocks
chameco Sep 30, 2022
2fb0a49
Address warning
chameco Sep 30, 2022
0c1b98b
Merge branch 'master' into sb/yosys
Oct 4, 2022
2664d83
Merge branch 'master' into sb/yosys
chameco Oct 7, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 2 additions & 0 deletions cabal.project
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions deps/language-sally
Open in desktop
Submodule language-sally added at de4f97
2 changes: 1 addition & 1 deletion deps/what4
Open in desktop
Submodule what4 updated 21 files
+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
Loading