| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| | | | | | |
|
| | | | | |
| | | | | |
| #include <linux/module.h>
#include "libgcc.h"
long long __ashrdi3(long long u, word_type b)
{
DWunion uu, w;
word_type bm;
if (b == 0)
return u;
uu.ll = u;
bm = 32 - b;
if (bm <= 0) {
/* w.s.high = 1..1 or 0..0 */
w.s.high =
uu.s.high >> 31;
w.s.low = uu.s.high >> -bm;
} else {
const unsigned int carries = (unsigned int) uu.s.high << bm;
w.s.high = |
| | | | | | |
|
|\ \ \ \ \ \
| |/ / / / /
|/| | | | | |
verific: enable import all cells
|
| | | | | | |
|
|/ / / / / |
|
| | | | | |
|
|\ \ \ \ \
| | | | | |
| | | | | | |
smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
|
|/ / / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The witness metadata was missing fine grained FFs completely and for
coarse grained FFs where the output connection has multiple chunks it
lacked the offset of the chunk within the SMT expression. This fixes
both, the later by adding an "smtoffset" field to the metadata.
|
|/ / / / |
|
|\ \ \ \
| | | | |
| | | | | |
equiv_opt and clk2fflogic fixes
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
| | | | |
| | | | |
| | | | |
| | | | | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
| | | | |
| | | | |
| | | | |
| | | | | |
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 08be796cb8b1890923e459cda92211fda763f0c1, reversing
changes made to 38dbb44fa0815b1fe80e68e17798aaa341d998cd.
This fixes #2728. PR #641 did not actually "fix" #639.
The actual issue in #639 is not equiv_make, but assumptions in equiv_simple
that are not true for the test case provided in #639.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is a complete rewrite of the FF replacing code.
The previous implementation tried to implement the negative hold time by
wrapping async control signals individually with pulse stretching. This
did not correctly model the interaction between different simultaneously
changing inputs (e.g. a falling ALOAD together with a changing AD would
load the changed AD instead of the value AD had when ALOAD was high; a
falling CLR could mask a raising SET for one cycle; etc.).
The new approach first has the logic for all updates using only sampled
values followed by the logic for all updates using only current values.
That way, e.g., a falling ALOAD will load the sampled AD value but a
still active ALOAD will load the current AD value.
The new code also has deterministic behavior for the initial state: no
operation is active when that operation would depend on a specific
previous signal value. This also means clk2fflogic will no longer
generate any additional uninitialized FFs.
I also documented the negative hold time behavior in the help message,
copying the relevant part from async2sync's help messages.
|
| | | | | |
|
|\ \ \ \ \
| | | | | |
| | | | | | |
backends: protobuf: removed protobuf backend
|
|/ / / / / |
|
| | | | | |
|
|\ \ \ \ \
| | | | | |
| | | | | | |
Add BLIF names command input plane size check
|