Functional Backend #4536

aiju · 2024-08-13T10:31:37Z

Add a new intermediate representation to be used for writing backends for functional language-shaped targets, conversion code from RTLIL, and three example backends (C++, SMTLIB and Rosette).

povik · 2024-08-13T11:17:48Z

Is this preserving undefined bits, or is this more of a synthesis target like CXXRTL?

aiju · 2024-08-13T11:32:46Z

Is this preserving undefined bits, or is this more of a synthesis target like CXXRTL?

Currently 'x' bits are treated as 'dont care' (mostly set to 0), which I think matches the existing formal infrastructure. The idea is that users can use xprop if they want 'x' behaviour.

povik · 2024-08-13T11:37:42Z

FWIW a write-up on how this differs from CXXRTL (apart from this being language-agnostic) would help me understand what this is. I know you all are busy though.

aiju · 2024-08-13T12:56:07Z

FWIW a write-up on how this differs from CXXRTL (apart from this being language-agnostic) would help me understand what this is. I know you all are busy though.

I don't actually know how CXXRTL works in detail but the key point is that this is intended to match formal semantics and I think CXXRTL is a mix of simulation and synthesis semantics.

whitequark · 2024-08-13T13:05:40Z

I don't actually know how CXXRTL works in detail but the key point is that this is intended to match formal semantics and I think CXXRTL is a mix of simulation and synthesis semantics.

CXXRTL implements synthesis semantics only, to my best knowledge. (Obviously, sometimes that would match simulation semantics.)

georgerennie · 2024-08-14T20:41:54Z

Currently 'x' bits are treated as 'dont care' (mostly set to 0), which I think matches the existing formal infrastructure

Is this just for the C++ target or also for smtlib/rosette? For C++ which requires concrete values this obviously makes sense to set to 0, but if being used with smtlib/rosette for verification surely you want to leave xs as symbolic variables that can take the value 0 or 1 (pseudo primary inputs, the same as $anyseq) to verify all allowed behaviours?

Existing formal infrastructure by default models xs in this way for this reason (although doesn't model x-prop semantics unless xprop is used)

KrystalDelusion · 2024-08-15T15:19:03Z

smtlib/rosette (currently) pull down to 0

aiju · 2024-08-21T06:59:01Z

Currently 'x' bits are treated as 'dont care' (mostly set to 0), which I think matches the existing formal infrastructure

Is this just for the C++ target or also for smtlib/rosette? For C++ which requires concrete values this obviously makes sense to set to 0, but if being used with smtlib/rosette for verification surely you want to leave xs as symbolic variables that can take the value 0 or 1 (pseudo primary inputs, the same as $anyseq) to verify all allowed behaviours?

Existing formal infrastructure by default models xs in this way for this reason (although doesn't model x-prop semantics unless xprop is used)

Oh I didn't know that's how it works. If it's just constants then that's probably not too difficult to add as an option. I bounced off x-semantics because adding x-propagation seemed too complicated and enforcing 2-value logic seemed like the easiest solution.

This adds a generic non-recursive implementation of Tarjan's linear time SCC algorithm that produces components in topological order. It can be instantiated to work directly on any graph representation for which the enumerate_nodes and enumerate_successors interface can be implemented.

When implementing custom log_... functions or custom overloads for the core log functions like log_signal it is necessary to return `char *` that are valid long enough. The log_... functions implemented in log.cc use either `log_id_cache` or `string_buf` which both are cleared on log_pop. This commit adds a public `log_str` function which stores its argument in the `log_id_cache` and returns the stored copy, such that custom log functions outside of log.cc can also create strings that remain valid until the next `log_pop`.

This is already supported by `SigSpec` and since both `SigChunk` and `SigSpec` implement `extract` which is the multi-bit variant of this, there is no good reason for `SigChunk` to not support `SigBit operator[](int offset)`.

It adds `DriveBit`, `DriveChunk` and `DriveSpec` types which are similar to `SigBit`, `SigChunk` and `SigSpec` but can also directly represent cell ports, undriven bits and multiple drivers. For indexing an RTLIL module and for querying signal drivers it comes with a `DriverMap` type which is somewhat similar to a `SigMap` but is guaranteed to produce signal drivers as returned representatives. A `DriverMap` can also optionally preserve connections via intermediate wires (e.g. querying the driver of a cell input port will return a connected intermediate wire, querying the driver of that wire will return the cell output port that's driving the wire).

…rivers

…unctional backend

…se it

…on with yosys sim

… below other definitions

…the terminology consistent

backends/functional/test_generic.cc

+			if(addr % 8 == 7) printf("\n");
+		}
+		printf("\n");
+		//log_abort();


backends/functional/test_generic.cc

+			//addr_t length = std::min((1<<addr_width) - low, length_dist(rnd));
+			//addr_t high = low + length - 1;


backends/functional/test_generic.cc

+/*
+		MemContentsTest test(8, 16);
+
+		std::random_device seed_dev;
+		std::mt19937 rnd(23); //seed_dev());
+		test.run(rnd, 1000);
+*/


kernel/drivertools.h

+inline DriveChunkMultiple::DriveChunkMultiple(DriveBitMultiple const &bit)
+	: width_(1)
+{
+	for (auto const &bit : bit.multiple())


kernel/functional.cc

+		} else if(cellType == ID($demux)) {
+			int width = parameters.at(ID(WIDTH)).as_int();
+			int s_width = parameters.at(ID(S_WIDTH)).as_int();
+			int y_width = width << s_width;


kernel/mem.h

+	// check if the iterator points to a range overlapping with [begin_addr, end_addr)
+	bool _range_overlaps(std::map<addr_t, RTLIL::Const>::iterator it, addr_t begin_addr, addr_t end_addr) const;
+	// return the offset the addr would have in the range at `it`
+	size_t _range_offset(std::map<addr_t, RTLIL::Const>::iterator it, addr_t addr) const { return (addr - it->first) * _data_width; }


kernel/sexpr.h

+public:
+	SExpr(std::string a) : _v(std::move(a)) {}
+    SExpr(const char *a) : _v(a) {}
+    // FIXME: should maybe be defined for all integral types


kernel/sexpr.h

+
+namespace SExprUtil {
+    // A little hack so that `using SExprUtil::list` lets you import a shortcut to `SExpr::list`
+    template<typename... Args> SExpr list(Args&&... args) {


kernel/sexpr.h

+
+namespace SExprUtil {
+    // A little hack so that `using SExprUtil::list` lets you import a shortcut to `SExpr::list`
+    template<typename... Args> SExpr list(Args&&... args) {


passes/cmds/example_dt.cc

+    }
+
+
+	void execute(std::vector<std::string> args, RTLIL::Design *design) override


Also unique_name can take field_name directly.

Note sure if this is the best way to do it, but it works?

Run functional tests on private runner only

KrystalDelusion

Missing smtlib and rosette tests, but that can be fixed later.

povik · 2024-09-06T10:08:59Z

backends/functional/cxx_runtime/sim.h

+template<size_t n>
+class Signal {
+    template<size_t m> friend class Signal;
+    std::array<bool, n> _bits;


Btw why this instead of std::bitset<n>?

i didn't know about std::bitset :) i guess rewriting it to use that would simplify the code a bit, but would still need to implement addition, etc

povik · 2024-09-06T10:10:40Z

backends/functional/test_generic.cc

+
+struct FunctionalTestGeneric : public Pass
+{
+	FunctionalTestGeneric() : Pass("test_generic", "test the generic compute graph") {}


I suggest we rename this to test_cgraph or similar. This has the potential to confuse people

yea i'm happy to rename this, also test_generic.cc needs some cleanup that i forgot to do...

povik · 2024-09-06T10:14:30Z

kernel/functional.cc

+	// any nodes untouched by this point are dead code and will be removed by permute
+    _graph.permute(perm);
+    if(scc) log_error("The design contains combinational loops. This is not supported by the functional backend. "
+		"Try `scc -select; simplemap; select -clear` to avoid this error.\n");


This might be an outstanding TODO but simplemap will leave around gate cells which are unsupported by the functional backend as of yet

oh yeah gate-level cells was on my TODO list but i didn't get around to it for the deliverable

aiju force-pushed the functional branch from 9fbb3c8 to 8e5dc7f Compare August 21, 2024 09:48

jix and others added 21 commits August 21, 2024 10:58

kernel/rtlil: Add SigBit operator[](int offset) to SigChunk

f24e253

This is already supported by `SigSpec` and since both `SigChunk` and `SigSpec` implement `extract` which is the multi-bit variant of this, there is no good reason for `SigChunk` to not support `SigBit operator[](int offset)`.

WIP temporary drivertools example

68c3a47

topo_scc: Add sources_first option

f29422f

ComputeGraph datatype for the upcoming functional backend

d4e3daa

fixup! drivertools: Utility code for indexing and traversing signal d…

d90268f

…rivers

fix bugs in drivertools

dd5ec84

add initial version of functional C++ backend

63dea89

add initial version of functional smtlib backend

7611dda

Add test_cell tests for C++ functional backend

720429b

Change assert to log_assert

76371d1

add support for memories to c++ and smtlib functional backends

7b29d17

sim.h cannot use log_assert because does not include yosys headers

3552a8a

need unsigned comparison when checking shift widths for overflow in f…

dbf2bc3

…unctional backend

add support for std::variant to hashlib

248d5f7

add new generic compute graph and rewrite c++ functional backend to u…

6f9e212

…se it

Initial functional SMT backend using functional IR

4e370f4

Add test for SMT backend. Tests if SMT is valid and compares simulati…

54225b5

…on with yosys sim

Remove unused includes

c6e1126

aiju added 7 commits August 22, 2024 10:40

drivertools: fix C++20 "incomplete type" error by moving constructors…

9b5e81b

… below other definitions

functional backend: missing includes for stl containers

761eff5

add functional ir documentation

459e6b9

functional backends: identifiers in c++/smtlib may not start with digits

b428bf4

functional backend: more documentation

27efed2

functional backend: rename "type" to either "kind" or "sort" to make …

4eeb8d3

…the terminology consistent

functional backend: add test to verify test_generic

2b8db94

github-advanced-security bot found potential problems Aug 29, 2024

View reviewed changes

KrystalDelusion and others added 12 commits September 3, 2024 11:32

smtr: Fork smtlib for rosette

8b29629

smtr: Add rkt to functional tests

7fe9157

smtr: Use rosette/safe

07b6908

smtr: More sanitization

5a29b3e

smtr: Use scope.unique_name

a2abbcb

smtr: Structs have local scope

d6c5e13

Also unique_name can take field_name directly.

fix rst formatting in functional_ir.rst

75ed6d3

functional_ir.rst: fix typo, document SExprWriter::flush

7de8be1

functional tests: run from make tests but not smtlib/rkt tests

5a476a8

Makefile: Update coverage_functional

21494d1

Note sure if this is the best way to do it, but it works?

Run functional tests on private runner only

fc10a6e

Merge pull request #4585 from YosysHQ/functional_tests

0ad2431

Run functional tests on private runner only

mmicko marked this pull request as ready for review September 6, 2024 07:52

mmicko requested review from mmicko and KrystalDelusion as code owners September 6, 2024 07:52

KrystalDelusion approved these changes Sep 6, 2024

View reviewed changes

mmicko approved these changes Sep 6, 2024

View reviewed changes

mmicko merged commit b20df72 into main Sep 6, 2024
29 checks passed

mmicko deleted the functional branch September 6, 2024 08:05

povik reviewed Sep 6, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Functional Backend #4536

Functional Backend #4536

aiju commented Aug 13, 2024

povik commented Aug 13, 2024

aiju commented Aug 13, 2024

povik commented Aug 13, 2024

aiju commented Aug 13, 2024

whitequark commented Aug 13, 2024

georgerennie commented Aug 14, 2024 •

edited

Loading

KrystalDelusion commented Aug 15, 2024

aiju commented Aug 21, 2024

KrystalDelusion left a comment

povik Sep 6, 2024

aiju Sep 10, 2024

povik Sep 6, 2024

aiju Sep 10, 2024 •

edited

Loading

povik Sep 6, 2024

aiju Sep 10, 2024

		//addr_t length = std::min((1<<addr_width) - low, length_dist(rnd));
		//addr_t high = low + length - 1;

		}


		void execute(std::vector<std::string> args, RTLIL::Design *design) override

Functional Backend #4536

Functional Backend #4536

Conversation

aiju commented Aug 13, 2024

povik commented Aug 13, 2024

aiju commented Aug 13, 2024

povik commented Aug 13, 2024

aiju commented Aug 13, 2024

whitequark commented Aug 13, 2024

georgerennie commented Aug 14, 2024 • edited Loading

KrystalDelusion commented Aug 15, 2024

aiju commented Aug 21, 2024

KrystalDelusion left a comment

Choose a reason for hiding this comment

povik Sep 6, 2024

Choose a reason for hiding this comment

aiju Sep 10, 2024

Choose a reason for hiding this comment

povik Sep 6, 2024

Choose a reason for hiding this comment

aiju Sep 10, 2024 • edited Loading

Choose a reason for hiding this comment

povik Sep 6, 2024

Choose a reason for hiding this comment

aiju Sep 10, 2024

Choose a reason for hiding this comment

georgerennie commented Aug 14, 2024 •

edited

Loading

aiju Sep 10, 2024 •

edited

Loading