aboutsummaryrefslogtreecommitdiffstats
path: root/examples
Commit message (Collapse)AuthorAgeFilesLines
* glift: Use `qbfsat -O2` instead of manually calling `abc`.Alberto Gonzalez2020-07-018-40/+8
|
* glift: Change command names to better represent their functions.Alberto Gonzalez2020-07-019-27/+27
|
* glift: Add `-create-imprecise` command, rename other commands, and re-work ↵Alberto Gonzalez2020-07-019-12/+13
| | | | the help text.
* glift: Add examples, including a number of benchmarks used in some academic ↵Alberto Gonzalez2020-07-0118-1/+7279
| | | | works.
* Use C++11 final/override keywords.whitequark2020-06-181-1/+1
|
* kernel: use more ID::*Eddie Hung2020-04-021-2/+2
|
* Add support for optimizing exists-forall problems.Alberto Gonzalez2020-03-132-2/+22
| | | | | | Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate. Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al. Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
* set undriven pads to zeroPepijn de Vos2019-09-041-2/+2
|
* fix tcl scriptPepijn de Vos2019-09-041-2/+1
|
* add broken TCL run scriptPepijn de Vos2019-09-042-0/+18
|
* Add demonstration of breakagePepijn de Vos2019-09-041-0/+1
| | | | Unused outputs lead to undriven buffers, which lead to syntax errors.
* Update example for GW1NR-9Pepijn de Vos2019-09-044-47/+28
| | | | This uses the Trenz TEC0117 on Gowin IDE 1.8.4
* Add clock buffer insertion pass, improve iopadmap.Marcin Kościelnicki2019-08-131-2/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A few new attributes are defined for use in cell libraries: - iopad_external_pin: marks PAD cell's external-facing pin. Pad insertion will be skipped for ports that are already connected to such a pin. - clkbuf_sink: marks an input pin as a clock pin, requesting clock buffer insertion. - clkbuf_driver: marks an output pin as a clock buffer output pin. Clock buffer insertion will be skipped for nets that are already driven by such a pin. All three are module attributes that should be set to a comma-separeted list of pin names. Clock buffer insertion itself works as follows: 1. All cell ports, starting from bottom up, can be marked as clock sinks (requesting clock buffer insertion) or as clock buffer outputs. 2. If a wire in a given module is driven by a cell port that is a clock buffer output, it is in turn also considered a clock buffer output. 3. If an input port in a non-top module is connected to a clock sink in a contained cell, it is also in turn considered a clock sink. 4. If a wire in a module is driven by a non-clock-buffer cell, and is also connected to a clock sink port in a contained cell, a clock buffer is inserted in this module. 5. For the top module, a clock buffer is also inserted on input ports connected to clock sinks, optionally with a special kind of input PAD (such as IBUFG for Xilinx). 6. Clock buffer insertion on a given wire is skipped if the clkbuf_inhibit attribute is set on it.
* Add a simple example for Spartan 6Marcin Kościelnicki2019-07-245-0/+47
|
* Added cell_stats exampleBenedikt Tutzer2019-04-034-478/+54
|
* Merge remote-tracking branch 'origin/master' into feature/python_bindingsBenedikt Tutzer2019-03-2816-1/+215
|\
| * Merge pull request #856 from kprasadvnsi/masterClifford Wolf2019-03-076-10/+12
| |\ | | | | | | examples/anlogic/ now also output the SVF file.
| | * examples/anlogic/ now also output the SVF file.Kali Prasad2019-03-066-10/+12
| | |
| * | Refactor SF2 iobuf insertion, Add clkint insertionClifford Wolf2019-03-061-1/+1
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * | Improve igloo2 exampleClifford Wolf2019-03-051-2/+3
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * | Improve igloo2 exampleClifford Wolf2019-03-052-2/+54
| | | | | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * | Improvements in SF2 flow and demoClifford Wolf2019-03-052-1/+2
| |/ | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Improve igloo2 exmapleClifford Wolf2019-03-054-8/+16
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Add missing newlineClifford Wolf2019-03-051-1/+1
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Added examples/anlogic/Kali Prasad2019-03-047-0/+55
| |
| * Improve igloo2 exampleClifford Wolf2019-03-032-3/+10
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Update igloo2 example to Libero v12.0Clifford Wolf2019-03-032-6/+5
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Cleanups in igloo2 example designClifford Wolf2019-01-176-7/+4
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Add SF2 IO buffer insertionClifford Wolf2019-01-172-2/+3
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Improve Igloo2 exampleClifford Wolf2019-01-178-22/+41
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Improve igloo2 exampleClifford Wolf2019-01-084-5/+29
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Add skeleton Yosys-Libero igloo2 example projectClifford Wolf2019-01-055-0/+44
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
| * Merge pull request #591 from hzeller/virtual-overrideClifford Wolf2018-08-151-1/+1
| |\ | | | | | | Consistent use of 'override' for virtual methods in derived classes.
| | * Consistent use of 'override' for virtual methods in derived classes.Henner Zeller2018-07-201-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | o Not all derived methods were marked 'override', but it is a great feature of C++11 that we should make use of. o While at it: touched header files got a -*- c++ -*- for emacs to provide support for that language. o use YS_OVERRIDE for all override keywords (though we should probably use the plain keyword going forward now that C++11 is established)
| * | fix basys3 examplejapm482018-07-222-0/+4
| |/ | | | | | | | | | | | | Added `CONFIG_VOLTAGE` and `CFGBVS` to constraints file to avoid warning `DRC 23-20`. Added `open_hw` needed for programming.
* / Added sample code for python-apiBenedikt Tutzer2018-12-113-0/+479
|/
* Update examples/cmos/counter.ys to use "synth" commandClifford Wolf2018-05-301-5/+5
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add smtbmc support for exist-forall problemsClifford Wolf2018-02-233-2/+23
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add $allconst and $allseq cell typesClifford Wolf2018-02-231-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fixed the -vout flag to -vqm in examples/intel directorydh732017-11-144-4/+4
|
* Add timing constraints to osu035 exampleClifford Wolf2017-10-103-2/+4
|
* Add examples/osu035Clifford Wolf2017-05-234-0/+30
|
* Replace CRLF line endings with LF in de2i.qsf (quartus example)Clifford Wolf2017-04-121-1098/+1098
|
* Squelch trailing whitespaceLarry Doolittle2017-04-126-31/+31
|
* Add initial support for both MAX10 and Cyclone IV (E|GX) FPGAsdh732017-04-0517-0/+1287
|
* Added $assert/$assume support to AIGER back-endClifford Wolf2016-12-032-3/+3
|
* Added examples/aiger/Clifford Wolf2016-12-014-0/+53
|
* Progress in examples/gowin/Clifford Wolf2016-11-085-21/+95
|
* Added examples/gowin/Clifford Wolf2016-11-076-0/+57
|
* Added $anyseq cell typeClifford Wolf2016-10-141-1/+2
|
generated by cgit v1.2.3 (git 2.25.1) at 2025-09-13 08:22:43 +0000
n> } // FindMaxBipartiteMatching and its helper class. // // Uses the well-known Ford-Fulkerson max flow method to find a maximum // bipartite matching. Flow is considered to be from left to right. // There is an implicit source node that is connected to all of the left // nodes, and an implicit sink node that is connected to all of the // right nodes. All edges have unit capacity. // // Neither the flow graph nor the residual flow graph are represented // explicitly. Instead, they are implied by the information in 'graph' and // a vector<int> called 'left_' whose elements are initialized to the // value kUnused. This represents the initial state of the algorithm, // where the flow graph is empty, and the residual flow graph has the // following edges: // - An edge from source to each left_ node // - An edge from each right_ node to sink // - An edge from each left_ node to each right_ node, if the // corresponding edge exists in 'graph'. // // When the TryAugment() method adds a flow, it sets left_[l] = r for some // nodes l and r. This induces the following changes: // - The edges (source, l), (l, r), and (r, sink) are added to the // flow graph. // - The same three edges are removed from the residual flow graph. // - The reverse edges (l, source), (r, l), and (sink, r) are added // to the residual flow graph, which is a directional graph // representing unused flow capacity. // // When the method augments a flow (moving left_[l] from some r1 to some // other r2), this can be thought of as "undoing" the above steps with // respect to r1 and "redoing" them with respect to r2. // // It bears repeating that the flow graph and residual flow graph are // never represented explicitly, but can be derived by looking at the // information in 'graph' and in left_. // // As an optimization, there is a second vector<int> called right_ which // does not provide any new information. Instead, it enables more // efficient queries about edges entering or leaving the right-side nodes // of the flow or residual flow graphs. The following invariants are // maintained: // // left[l] == kUnused or right[left[l]] == l // right[r] == kUnused or left[right[r]] == r // // . [ source ] . // . ||| . // . ||| . // . ||\--> left[0]=1 ---\ right[0]=-1 ----\ . // . || | | . // . |\---> left[1]=-1 \--> right[1]=0 ---\| . // . | || . // . \----> left[2]=2 ------> right[2]=2 --\|| . // . ||| . // . elements matchers vvv . // . [ sink ] . // // See Also: // [1] Cormen, et al (2001). "Section 26.2: The Ford-Fulkerson method". // "Introduction to Algorithms (Second ed.)", pp. 651-664. // [2] "Ford-Fulkerson algorithm", Wikipedia, // 'http://en.wikipedia.org/wiki/Ford%E2%80%93Fulkerson_algorithm' class MaxBipartiteMatchState { public: explicit MaxBipartiteMatchState(const MatchMatrix& graph) : graph_(&graph), left_(graph_->LhsSize(), kUnused), right_(graph_->RhsSize(), kUnused) { } // Returns the edges of a maximal match, each in the form {left, right}. ElementMatcherPairs Compute() { // 'seen' is used for path finding { 0: unseen, 1: seen }. ::std::vector<char> seen; // Searches the residual flow graph for a path from each left node to // the sink in the residual flow graph, and if one is found, add flow // to the graph. It's okay to search through the left nodes once. The // edge from the implicit source node to each previously-visited left // node will have flow if that left node has any path to the sink // whatsoever. Subsequent augmentations can only add flow to the // network, and cannot take away that previous flow unit from the source. // Since the source-to-left edge can only carry one flow unit (or, // each element can be matched to only one matcher), there is no need // to visit the left nodes more than once looking for augmented paths. // The flow is known to be possible or impossible by looking at the // node once. for (size_t ilhs = 0; ilhs < graph_->LhsSize(); ++ilhs) { // Reset the path-marking vector and try to find a path from // source to sink starting at the left_[ilhs] node. GTEST_CHECK_(left_[ilhs] == kUnused) << "ilhs: " << ilhs << ", left_[ilhs]: " << left_[ilhs]; // 'seen' initialized to 'graph_->RhsSize()' copies of 0. seen.assign(graph_->RhsSize(), 0); TryAugment(ilhs, &seen); } ElementMatcherPairs result; for (size_t ilhs = 0; ilhs < left_.size(); ++ilhs) { size_t irhs = left_[ilhs]; if (irhs == kUnused) continue; result.push_back(ElementMatcherPair(ilhs, irhs)); } return result; } private: static const size_t kUnused = static_cast<size_t>(-1); // Perform a depth-first search from left node ilhs to the sink. If a // path is found, flow is added to the network by linking the left and // right vector elements corresponding each segment of the path. // Returns true if a path to sink was found, which means that a unit of // flow was added to the network. The 'seen' vector elements correspond // to right nodes and are marked to eliminate cycles from the search. // // Left nodes will only be explored at most once because they // are accessible from at most one right node in the residual flow // graph. // // Note that left_[ilhs] is the only element of left_ that TryAugment will // potentially transition from kUnused to another value. Any other // left_ element holding kUnused before TryAugment will be holding it // when TryAugment returns. // bool TryAugment(size_t ilhs, ::std::vector<char>* seen) { for (size_t irhs = 0; irhs < graph_->RhsSize(); ++irhs) { if ((*seen)[irhs]) continue; if (!graph_->HasEdge(ilhs, irhs)) continue; // There's an available edge from ilhs to irhs. (*seen)[irhs] = 1; // Next a search is performed to determine whether // this edge is a dead end or leads to the sink. // // right_[irhs] == kUnused means that there is residual flow from // right node irhs to the sink, so we can use that to finish this // flow path and return success. // // Otherwise there is residual flow to some ilhs. We push flow // along that path and call ourselves recursively to see if this // ultimately leads to sink. if (right_[irhs] == kUnused || TryAugment(right_[irhs], seen)) { // Add flow from left_[ilhs] to right_[irhs]. left_[ilhs] = irhs; right_[irhs] = ilhs; return true; } } return false; } const MatchMatrix* graph_; // not owned // Each element of the left_ vector represents a left hand side node // (i.e. an element) and each element of right_ is a right hand side // node (i.e. a matcher). The values in the left_ vector indicate // outflow from that node to a node on the the right_ side. The values // in the right_ indicate inflow, and specify which left_ node is // feeding that right_ node, if any. For example, left_[3] == 1 means // there's a flow from element #3 to matcher #1. Such a flow would also // be redundantly represented in the right_ vector as right_[1] == 3. // Elements of left_ and right_ are either kUnused or mutually // referent. Mutually referent means that left_[right_[i]] = i and // right_[left_[i]] = i. ::std::vector<size_t> left_; ::std::vector<size_t> right_; GTEST_DISALLOW_ASSIGN_(MaxBipartiteMatchState); }; const size_t MaxBipartiteMatchState::kUnused; GTEST_API_ ElementMatcherPairs FindMaxBipartiteMatching(const MatchMatrix& g) { return MaxBipartiteMatchState(g).Compute(); } static void LogElementMatcherPairVec(const ElementMatcherPairs& pairs, ::std::ostream* stream) { typedef ElementMatcherPairs::const_iterator Iter; ::std::ostream& os = *stream; os << "{"; const char *sep = ""; for (Iter it = pairs.begin(); it != pairs.end(); ++it) { os << sep << "\n (" << "element #" << it->first << ", " << "matcher #" << it->second << ")"; sep = ","; } os << "\n}"; } // Tries to find a pairing, and explains the result. GTEST_API_ bool FindPairing(const MatchMatrix& matrix, MatchResultListener* listener) { ElementMatcherPairs matches = FindMaxBipartiteMatching(matrix); size_t max_flow = matches.size(); bool result = (max_flow == matrix.RhsSize()); if (!result) { if (listener->IsInterested()) { *listener << "where no permutation of the elements can " "satisfy all matchers, and the closest match is " << max_flow << " of " << matrix.RhsSize() << " matchers with the pairings:\n"; LogElementMatcherPairVec(matches, listener->stream()); } return false; } if (matches.size() > 1) { if (listener->IsInterested()) { const char *sep = "where:\n"; for (size_t mi = 0; mi < matches.size(); ++mi) { *listener << sep << " - element #" << matches[mi].first << " is matched by matcher #" << matches[mi].second; sep = ",\n"; } } } return true; } bool MatchMatrix::NextGraph() { for (size_t ilhs = 0; ilhs < LhsSize(); ++ilhs) { for (size_t irhs = 0; irhs < RhsSize(); ++irhs) { char& b = matched_[SpaceIndex(ilhs, irhs)]; if (!b) { b = 1; return true; } b = 0; } } return false; } void MatchMatrix::Randomize() { for (size_t ilhs = 0; ilhs < LhsSize(); ++ilhs) { for (size_t irhs = 0; irhs < RhsSize(); ++irhs) { char& b = matched_[SpaceIndex(ilhs, irhs)]; b = static_cast<char>(rand() & 1); // NOLINT } } } string MatchMatrix::DebugString() const { ::std::stringstream ss; const char *sep = ""; for (size_t i = 0; i < LhsSize(); ++i) { ss << sep; for (size_t j = 0; j < RhsSize(); ++j) { ss << HasEdge(i, j); } sep = ";"; } return ss.str(); } void UnorderedElementsAreMatcherImplBase::DescribeToImpl( ::std::ostream* os) const { if (matcher_describers_.empty()) { *os << "is empty"; return; } if (matcher_describers_.size() == 1) { *os << "has " << Elements(1) << " and that element "; matcher_describers_[0]->DescribeTo(os); return; } *os << "has " << Elements(matcher_describers_.size()) << " and there exists some permutation of elements such that:\n"; const char* sep = ""; for (size_t i = 0; i != matcher_describers_.size(); ++i) { *os << sep << " - element #" << i << " "; matcher_describers_[i]->DescribeTo(os); sep = ", and\n"; } } void UnorderedElementsAreMatcherImplBase::DescribeNegationToImpl( ::std::ostream* os) const { if (matcher_describers_.empty()) { *os << "isn't empty"; return; } if (matcher_describers_.size() == 1) { *os << "doesn't have " << Elements(1) << ", or has " << Elements(1) << " that "; matcher_describers_[0]->DescribeNegationTo(os); return; } *os << "doesn't have " << Elements(matcher_describers_.size()) << ", or there exists no permutation of elements such that:\n"; const char* sep = ""; for (size_t i = 0; i != matcher_describers_.size(); ++i) { *os << sep << " - element #" << i << " "; matcher_describers_[i]->DescribeTo(os); sep = ", and\n"; } } // Checks that all matchers match at least one element, and that all // elements match at least one matcher. This enables faster matching // and better error reporting. // Returns false, writing an explanation to 'listener', if and only // if the success criteria are not met. bool UnorderedElementsAreMatcherImplBase:: VerifyAllElementsAndMatchersAreMatched( const ::std::vector<string>& element_printouts, const MatchMatrix& matrix, MatchResultListener* listener) const { bool result = true; ::std::vector<char> element_matched(matrix.LhsSize(), 0); ::std::vector<char> matcher_matched(matrix.RhsSize(), 0); for (size_t ilhs = 0; ilhs < matrix.LhsSize(); ilhs++) { for (size_t irhs = 0; irhs < matrix.RhsSize(); irhs++) { char matched = matrix.HasEdge(ilhs, irhs); element_matched[ilhs] |= matched; matcher_matched[irhs] |= matched; } } { const char* sep = "where the following matchers don't match any elements:\n"; for (size_t mi = 0; mi < matcher_matched.size(); ++mi) { if (matcher_matched[mi]) continue; result = false; if (listener->IsInterested()) { *listener << sep << "matcher #" << mi << ": "; matcher_describers_[mi]->DescribeTo(listener->stream()); sep = ",\n"; } } } { const char* sep = "where the following elements don't match any matchers:\n"; const char* outer_sep = ""; if (!result) { outer_sep = "\nand "; } for (size_t ei = 0; ei < element_matched.size(); ++ei) { if (element_matched[ei]) continue; result = false; if (listener->IsInterested()) { *listener << outer_sep << sep << "element #" << ei << ": " << element_printouts[ei]; sep = ",\n"; outer_sep = ""; } } } return result; } } // namespace internal } // namespace testing
generated by cgit v1.2.3 (git 2.25.1) at 2025-09-13 08:22:43 +0000