29 commits

Author	SHA1	Message	Date
Robert O'Callahan	e0ae7b7af4	Remove .c_str() calls from log()/log_error() ... There are some leftovers, but this is an easy regex-based approach that removes most of them.	2025-09-11 20:59:37 +00:00
Emily Schmidt	4eeb8d326a	functional backend: rename "type" to either "kind" or "sort" to make the terminology consistent	2024-08-28 12:39:41 +01:00
Emily Schmidt	b428bf4600	functional backends: identifiers in c++/smtlib may not start with digits	2024-08-27 13:10:34 +01:00
Emily Schmidt	f456761e88	add sandia copyright notice to the functional backend	2024-08-21 11:04:11 +01:00
Emily Schmidt	50047d25b3	functional backend: add different types of input/output/state variables	2024-08-21 11:04:11 +01:00
Emily Schmidt	850b3a6c29	convert class FunctionalIR to a namespace Functional, rename functionalir.h to functional.h, rename functional.h to compute_graph.h	2024-08-21 11:04:08 +01:00
Emily Schmidt	99effb6789	add support for initializing registers and memories to the functional backend	2024-08-21 11:03:29 +01:00
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