Emily Schmidt
|
6d329e142d
|
functional backend: error out if multiply driven or undriven signals are seen, dont bother putting them in functionalir
|
2024-08-21 11:03:29 +01:00 |
Emily Schmidt
|
13bacc5c8f
|
eliminate pmux in functional backend
|
2024-08-21 11:03:29 +01:00 |
Emily Schmidt
|
55c2c17853
|
document functionalir.h and change visitors to derive from AbstractVisitor. remove extraneous widths arguments from visitors.
|
2024-08-21 11:03:29 +01:00 |
Emily Schmidt
|
6e7ae88c6a
|
fix bugs in smtlib backend
|
2024-08-21 11:03:29 +01:00 |
Emily Schmidt
|
00a65754bb
|
factor out SExpr/SExprWriter classes out of smtlib backend, and also tidy them up/document them
|
2024-08-21 11:03:27 +01:00 |
Emily Schmidt
|
c659ef29f4
|
change smtlib backend to use list() function instead of SExpr{} constructor (leads to weird constructor overloading resolution issues)
|
2024-08-21 11:02:31 +01:00 |
Emily Schmidt
|
9f660b1e4b
|
rewrite smtlib pass to use SExpr class
|
2024-08-21 11:02:31 +01:00 |
Roland Coeurjoly
|
7cff8fa3a3
|
Fix corner case of pos cell with input and output being same width
|
2024-08-21 11:02:31 +01:00 |
Roland Coeurjoly
|
fad76ce677
|
Fix memory leak
|
2024-08-21 11:02:31 +01:00 |
Roland Coeurjoly
|
5780357cd9
|
Emit valid SMT for stateful designs, fix some cells
|
2024-08-21 11:02:31 +01:00 |
Emily Schmidt
|
1b2986f7fb
|
add support for $mul, $div, $divfloor, $mod, $modfloor, $pow in functional backend
|
2024-08-21 11:02:31 +01:00 |
Roland Coeurjoly
|
32cdf25838
|
Use FunctionalTools::Scope instead of replaceCharacters
|
2024-08-21 11:02:31 +01:00 |
Roland Coeurjoly
|
ee6bd59436
|
Removed unnecesary nested_lets variable, use writer.print instead
|
2024-08-21 11:02:31 +01:00 |
Roland Coeurjoly
|
4109fcedcf
|
clang-format smtlib.cc
|
2024-08-21 11:02:31 +01:00 |
Roland Coeurjoly
|
94ddbc9577
|
Fix reduce_or
|
2024-08-21 11:02:31 +01:00 |
Roland Coeurjoly
|
b98210d8ac
|
Valid SMT is emitted, improved test script
|
2024-08-21 11:02:31 +01:00 |
Roland Coeurjoly
|
c6e112686c
|
Remove unused includes
|
2024-08-21 11:02:31 +01:00 |
Roland Coeurjoly
|
4e370f4426
|
Initial functional SMT backend using functional IR
|
2024-08-21 11:02:31 +01:00 |
Emily Schmidt
|
7b29d177ac
|
add support for memories to c++ and smtlib functional backends
|
2024-08-21 11:01:09 +01:00 |
Roland Coeurjoly
|
76371d177f
|
Change assert to log_assert
|
2024-08-21 11:01:09 +01:00 |
Roland Coeurjoly
|
720429b1fd
|
Add test_cell tests for C++ functional backend
|
2024-08-21 11:01:09 +01:00 |
Emily Schmidt
|
7611dda2eb
|
add initial version of functional smtlib backend
|
2024-08-21 11:01:09 +01:00 |