yosys/passes/sat
Jannis Harder 925f92918a clk2fflogic: Always correctly handle simultaneously changing signals
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.
2022-10-07 16:04:51 +02:00
..
Makefile.inc Add the $anyinit cell and the formalff pass 2022-08-16 13:37:30 +02:00
assertpmux.cc Fixing old e-mail addresses and deadnames 2021-06-08 00:39:36 +02:00
async2sync.cc async2sync: turn FFs with const clks into gclk FFs with feedback 2022-06-30 12:09:04 +02:00
clk2fflogic.cc clk2fflogic: Always correctly handle simultaneously changing signals 2022-10-07 16:04:51 +02:00
cutpoint.cc Fixing old e-mail addresses and deadnames 2021-06-08 00:39:36 +02:00
eval.cc Use HTTPS for website links, gatecat email 2021-06-09 12:16:56 +02:00
example.v Added support for shifter cells to SAT generator 2013-06-08 15:12:08 +02:00
example.ys Fixes in old SAT example.ys 2014-09-01 11:45:47 +02:00
expose.cc Fixing old e-mail addresses and deadnames 2021-06-08 00:39:36 +02:00
fmcombine.cc fmcombine: Add _gold/_gate suffix to memids 2022-06-03 21:52:28 +02:00
fminit.cc Fixing old e-mail addresses and deadnames 2021-06-08 00:39:36 +02:00
formalff.cc formalff: New -setundef option 2022-08-16 13:37:30 +02:00
freduce.cc Fixing old e-mail addresses and deadnames 2021-06-08 00:39:36 +02:00
miter.cc Fixing old e-mail addresses and deadnames 2021-06-08 00:39:36 +02:00
mutate.cc mutate: warn if less mutations possible than number requested 2022-10-05 10:59:38 +02:00
qbfsat.cc Fitting help messages to 80 character width 2022-08-24 10:40:57 +12:00
qbfsat.h qbfsat: Add `-solver-option` option. 2020-07-20 21:54:56 +00:00
sat.cc Fixing old e-mail addresses and deadnames 2021-06-08 00:39:36 +02:00
sim.cc Fitting help messages to 80 character width 2022-08-24 10:40:57 +12:00
supercover.cc Fixing old e-mail addresses and deadnames 2021-06-08 00:39:36 +02:00