diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 5 | ||||
| -rw-r--r-- | passes/sat/sim.cc | 5 | ||||
| -rw-r--r-- | techlibs/ecp5/cells_sim.v | 43 |
4 files changed, 22 insertions, 33 deletions
@@ -129,7 +129,7 @@ LDFLAGS += -rdynamic LDLIBS += -lrt endif -YOSYS_VER := 0.14+42 +YOSYS_VER := 0.14+51 GIT_REV := $(shell git -C $(YOSYS_SRC) rev-parse --short HEAD 2> /dev/null || echo UNKNOWN) OBJS = kernel/version_$(GIT_REV).o diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index e5cfcdc08..7e0d8f571 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -583,7 +583,10 @@ if aimfile is not None: if not got_topt: skip_steps = max(skip_steps, step) - num_steps = max(num_steps, step+1) + # some solvers optimize the properties so that they fail one cycle early, + # thus we check the properties in the cycle the aiger witness ends, and + # if that doesn't work, we check the cycle after that as well. + num_steps = max(num_steps, step+2) step += 1 if btorwitfile is not None: diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 9ee5d219c..ff3a30889 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -487,14 +487,13 @@ struct SimInstance if (ff_data.pol_clk ? (ff.past_clk == State::S0 && current_clk != State::S0) : (ff.past_clk == State::S1 && current_clk != State::S1)) { bool ce = ff.past_ce == (ff_data.pol_ce ? State::S1 : State::S0); - // chip enable priority over reset - if (ff_data.ce_over_srst && ff_data.has_ce && !ce) continue; // set if no ce, or ce is enabled if (!ff_data.has_ce || (ff_data.has_ce && ce)) { current_q = ff.past_d; } // override if sync reset - if ((ff_data.has_srst) && (ff.past_srst == (ff_data.pol_srst ? State::S1 : State::S0))) { + if ((ff_data.has_srst) && (ff.past_srst == (ff_data.pol_srst ? State::S1 : State::S0)) && + ((!ff_data.ce_over_srst) || (ff_data.ce_over_srst && ce))) { current_q = ff_data.val_srst; } } diff --git a/techlibs/ecp5/cells_sim.v b/techlibs/ecp5/cells_sim.v index a5f905cf8..76099f493 100644 --- a/techlibs/ecp5/cells_sim.v +++ b/techlibs/ecp5/cells_sim.v @@ -355,37 +355,24 @@ module TRELLIS_FF(input CLK, LSR, CE, DI, M, output reg Q); end endgenerate - generate - // TODO - if (CLKMUX == "INV") - specify - $setup(DI, negedge CLK, 0); - $setup(CE, negedge CLK, 0); - $setup(LSR, negedge CLK, 0); -`ifndef YOSYS - if (SRMODE == "ASYNC" && muxlsr) (negedge CLK => (Q : srval)) = 0; -`else - if (SRMODE == "ASYNC" && muxlsr) (LSR => Q) = 0; // Technically, this should be an edge sensitive path - // but for facilitating a bypass box, let's pretend it's - // a simple path -`endif - if (!muxlsr && muxce) (negedge CLK => (Q : DI)) = 0; - endspecify - else - specify - $setup(DI, posedge CLK, 0); - $setup(CE, posedge CLK, 0); - $setup(LSR, posedge CLK, 0); + specify + $setup(DI, negedge CLK &&& CLKMUX == "INV", 0); + $setup(CE, negedge CLK &&& CLKMUX == "INV", 0); + $setup(LSR, negedge CLK &&& CLKMUX == "INV", 0); + $setup(DI, posedge CLK &&& CLKMUX != "INV", 0); + $setup(CE, posedge CLK &&& CLKMUX != "INV", 0); + $setup(LSR, posedge CLK &&& CLKMUX != "INV", 0); `ifndef YOSYS - if (SRMODE == "ASYNC" && muxlsr) (posedge CLK => (Q : srval)) = 0; + if (SRMODE == "ASYNC" && muxlsr && CLKMUX == "INV") (negedge CLK => (Q : srval)) = 0; + if (SRMODE == "ASYNC" && muxlsr && CLKMUX != "INV") (posedge CLK => (Q : srval)) = 0; `else - if (SRMODE == "ASYNC" && muxlsr) (LSR => Q) = 0; // Technically, this should be an edge sensitive path - // but for facilitating a bypass box, let's pretend it's - // a simple path + if (SRMODE == "ASYNC" && muxlsr) (LSR => Q) = 0; // Technically, this should be an edge sensitive path + // but for facilitating a bypass box, let's pretend it's + // a simple path `endif - if (!muxlsr && muxce) (posedge CLK => (Q : DI)) = 0; - endspecify - endgenerate + if (!muxlsr && muxce && CLKMUX == "INV") (negedge CLK => (Q : DI)) = 0; + if (!muxlsr && muxce && CLKMUX != "INV") (posedge CLK => (Q : DI)) = 0; + endspecify endmodule // --------------------------------------- |