Functional backend

Makefile

@@ -558,6 +558,7 @@ $(eval $(call add_include_file,kernel/celltypes.h))
 $(eval $(call add_include_file,kernel/consteval.h))
 $(eval $(call add_include_file,kernel/constids.inc))
 $(eval $(call add_include_file,kernel/cost.h))
+$(eval $(call add_include_file,kernel/drivertools.h))
 $(eval $(call add_include_file,kernel/ff.h))
 $(eval $(call add_include_file,kernel/ffinit.h))
 $(eval $(call add_include_file,kernel/ffmerge.h))
@@ -598,6 +599,7 @@ $(eval $(call add_include_file,backends/rtlil/rtlil_backend.h))
 OBJS += kernel/driver.o kernel/register.o kernel/rtlil.o kernel/log.o kernel/calc.o kernel/yosys.o
 OBJS += kernel/binding.o
 OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/scopeinfo.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o kernel/fmt.o
+OBJS += kernel/drivertools.o
 ifeq ($(ENABLE_ZLIB),1)
 OBJS += kernel/fstdata.o
 endif
@@ -847,6 +849,8 @@ endif
 	+cd tests/xprop && bash run-test.sh $(SEEDOPT)
 	+cd tests/fmt && bash run-test.sh
 	+cd tests/cxxrtl && bash run-test.sh
+	+cd tests/functional/single_bit && bash run-test.sh
+	+cd tests/functional/multi_bit && bash run-test.sh
 	@echo ""
 	@echo "  Passed \"make test\"."
 	@echo ""

a.cc

@@ -0,0 +1,32 @@
+#include "sim.h"
+struct my_module_Inputs {
+	Signal<1> b;
+	Signal<1> a;
+
+	template <typename T> void dump(T &out) {
+		out("b", b);
+		out("a", a);
+	}
+};
+
+struct my_module_Outputs {
+	Signal<1> sum;
+
+	template <typename T> void dump(T &out) {
+		out("sum", sum);
+	}
+};
+
+struct my_module_State {
+
+	template <typename T> void dump(T &out) {
+	}
+};
+
+void my_module(my_module_Inputs const &input, my_module_Outputs &output, my_module_State const &current_state, my_module_State &next_state)
+{
+	Signal<1> b = input.b;
+	Signal<1> a = input.a;
+	Signal<1> $add$tests_functional_single_bit_verilog_my_module_add_v_7$1$_Y = $add(a, b); //
+	output.sum = $add$tests_functional_single_bit_verilog_my_module_add_v_7$1$_Y;
+}

add.cc

@@ -0,0 +1,32 @@
+#include "sim.h"
+struct my_module_Inputs {
+	Signal<1> b;
+	Signal<1> a;
+
+	template <typename T> void dump(T &out) {
+		out("b", b);
+		out("a", a);
+	}
+};
+
+struct my_module_Outputs {
+	Signal<1> sum;
+
+	template <typename T> void dump(T &out) {
+		out("sum", sum);
+	}
+};
+
+struct my_module_State {
+
+	template <typename T> void dump(T &out) {
+	}
+};
+
+void my_module(my_module_Inputs const &input, my_module_Outputs &output, my_module_State const &current_state, my_module_State &next_state)
+{
+	Signal<1> b = input.b;
+	Signal<1> a = input.a;
+	Signal<1> $add$tests_functional_single_bit_verilog_my_module_add_v_7$1$_Y = $add(a, b); //
+	output.sum = $add$tests_functional_single_bit_verilog_my_module_add_v_7$1$_Y;
+}

add.smt2

@@ -0,0 +1,22 @@
+; SMT-LIBv2 description generated by Yosys 0.41+101 (git sha1 52cc2ae5c, g++ 11.4.0-1ubuntu1~22.04 -fPIC -Os)
+; yosys-smt2-module my_module
+(declare-sort |my_module_s| 0)
+(declare-fun |my_module_is| (|my_module_s|) Bool)
+(declare-fun |my_module#0| (|my_module_s|) (_ BitVec 1)) ; \a
+(declare-fun |my_module#1| (|my_module_s|) (_ BitVec 1)) ; \b
+(define-fun |my_module#2| ((state |my_module_s|)) (_ BitVec 1) (bvadd (|my_module#0| state) (|my_module#1| state))) ; $add$tests/functional/single_bit/verilog/my_module_add.v:7$1_Y
+; yosys-smt2-output sum 1
+(define-fun |my_module_n sum| ((state |my_module_s|)) Bool (= ((_ extract 0 0) (|my_module#2| state)) #b1))
+; yosys-smt2-input b 1
+; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "smtoffset": 0, "type": "input", "width": 1}
+(define-fun |my_module_n b| ((state |my_module_s|)) Bool (= ((_ extract 0 0) (|my_module#1| state)) #b1))
+; yosys-smt2-input a 1
+; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "smtoffset": 0, "type": "input", "width": 1}
+(define-fun |my_module_n a| ((state |my_module_s|)) Bool (= ((_ extract 0 0) (|my_module#0| state)) #b1))
+(define-fun |my_module_a| ((state |my_module_s|)) Bool true)
+(define-fun |my_module_u| ((state |my_module_s|)) Bool true)
+(define-fun |my_module_i| ((state |my_module_s|)) Bool true)
+(define-fun |my_module_h| ((state |my_module_s|)) Bool true)
+(define-fun |my_module_t| ((state |my_module_s|) (next_state |my_module_s|)) Bool true) ; end of module my_module
+; yosys-smt2-topmod my_module
+; end of yosys output

and.cc

@@ -0,0 +1,32 @@
+#include "sim.h"
+struct my_module_Inputs {
+	Signal<1> b;
+	Signal<1> a;
+
+	template <typename T> void dump(T &out) {
+		out("b", b);
+		out("a", a);
+	}
+};
+
+struct my_module_Outputs {
+	Signal<1> sum;
+
+	template <typename T> void dump(T &out) {
+		out("sum", sum);
+	}
+};
+
+struct my_module_State {
+
+	template <typename T> void dump(T &out) {
+	}
+};
+
+void my_module(my_module_Inputs const &input, my_module_Outputs &output, my_module_State const &current_state, my_module_State &next_state)
+{
+	Signal<1> b = input.b;
+	Signal<1> a = input.a;
+	Signal<1> $add$tests_functional_single_bit_verilog_my_module_add_v_7$1$_Y = $add(a, b); //
+	output.sum = $add$tests_functional_single_bit_verilog_my_module_add_v_7$1$_Y;
+}

and.smt

@@ -0,0 +1,23 @@
+(declare-datatype my_module_inputs ((my_module_inputs
+  (my_module_inputs_b (_ BitVec 1))
+  (my_module_inputs_a (_ BitVec 1))
+)))
+(declare-datatype my_module_outputs ((my_module_outputs
+  (my_module_outputs_sum (_ BitVec 1))
+)))
+(declare-datatype my_module_state ((my_module_state
+)))
+(declare-datatypes ((Pair 2)) ((par (X Y) ((pair (first X) (second Y))))))
+(define-fun my_module_step ((inputs my_module_inputs) (current_state my_module_state)) (Pair my_module_outputs my_module_state)
+  (let (((b (my_module_inputs_b inputs))))
+  (let (((a (my_module_inputs_a inputs))))
+  (let ((($add$tests/functional/single_bit/verilog/my_module_add.v_7$1$_Y (bvadd a b))))
+    (pair 
+      (my_module_outputs
+        $add$tests/functional/single_bit/verilog/my_module_add.v_7$1$_Y    ; sum
+      )
+      (my_module_state
+      )
+    )
+  )))
+)

backends/functional/Makefile.inc

@@ -0,0 +1,4 @@
+OBJS += backends/functional/cxx.o
+# OBJS += backends/functional/smtlib.o
+# OBJS += backends/functional/alternative_cxx.o
+# OBJS += backends/functional/alternative_smtlib.o