aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGELOG1
-rw-r--r--backends/aiger/xaiger.cc20
-rw-r--r--frontends/verilog/verilog_lexer.l2
-rw-r--r--frontends/verilog/verilog_parser.y95
-rw-r--r--kernel/yosys.cc4
-rw-r--r--manual/CHAPTER_Overview.tex5
-rw-r--r--misc/py_wrap_generator.py3
-rw-r--r--passes/memory/memory_dff.cc8
-rw-r--r--passes/opt/wreduce.cc2
-rw-r--r--passes/techmap/muxcover.cc27
-rw-r--r--techlibs/common/synth.cc15
-rw-r--r--techlibs/intel/synth_intel.cc3
-rw-r--r--tests/memories/read_two_mux.v16
-rwxr-xr-xtests/memories/run-test.sh4
-rw-r--r--tests/various/abc9.v4
-rw-r--r--tests/various/abc9.ys10
-rw-r--r--tests/various/specify.v11
-rw-r--r--tests/various/specify.ys2
18 files changed, 128 insertions, 104 deletions
diff --git a/CHANGELOG b/CHANGELOG
index ae7d28236..646d63a63 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -12,6 +12,7 @@ Yosys 0.9 .. Yosys 0.9-dev
- Added "synth_xilinx -abc9" (experimental)
- Added "synth_ice40 -abc9" (experimental)
- Added "synth -abc9" (experimental)
+ - Added "synth -keepdc"
- Added "script -scriptwire
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index eb3d47569..869b741a6 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -138,6 +138,7 @@ struct XAigerWriter
{
pool<SigBit> undriven_bits;
pool<SigBit> unused_bits;
+ pool<SigBit> keep_bits;
// promote public wires
for (auto wire : module->wires())
@@ -168,6 +169,9 @@ struct XAigerWriter
unused_bits.insert(bit);
}
+ if (keep)
+ keep_bits.insert(bit);
+
if (wire->port_input || keep) {
if (bit != wirebit)
alias_map[bit] = wirebit;
@@ -235,7 +239,7 @@ struct XAigerWriter
log_assert(!holes_mode);
RTLIL::Module* inst_module = module->design->module(cell->type);
- if (inst_module && inst_module->attributes.count("\\abc_box_id")) {
+ if (inst_module && inst_module->attributes.count("\\abc_box_id")) {
abc_box_seen = true;
if (!holes_mode) {
@@ -255,10 +259,11 @@ struct XAigerWriter
}
}
else {
+ bool cell_known = cell->known();
for (const auto &c : cell->connections()) {
if (c.second.is_fully_const()) continue;
- auto is_input = cell->input(c.first);
- auto is_output = cell->output(c.first);
+ auto is_input = !cell_known || cell->input(c.first);
+ auto is_output = !cell_known || cell->output(c.first);
if (!is_input && !is_output)
log_error("Connection '%s' on cell '%s' (type '%s') not recognised!\n", log_id(c.first), log_id(cell), log_id(cell->type));
@@ -266,12 +271,15 @@ struct XAigerWriter
for (auto b : c.second.bits()) {
Wire *w = b.wire;
if (!w) continue;
- if (!w->port_output) {
+ if (!w->port_output || !cell_known) {
SigBit I = sigmap(b);
if (I != b)
alias_map[b] = I;
output_bits.insert(b);
unused_bits.erase(b);
+
+ if (!cell_known)
+ keep_bits.insert(b);
}
}
}
@@ -424,7 +432,7 @@ struct XAigerWriter
auto jt = input_bits.find(b);
if (jt != input_bits.end()) {
- log_assert(b.wire->attributes.count("\\keep"));
+ log_assert(keep_bits.count(O));
input_bits.erase(b);
}
}
@@ -444,7 +452,7 @@ struct XAigerWriter
// with $inout.out suffix, make it a PO driven by the existing inout, and
// inherit existing inout's drivers
if ((wire->port_input && wire->port_output && !undriven_bits.count(bit))
- || wire->attributes.count("\\keep")) {
+ || keep_bits.count(bit)) {
RTLIL::IdString wire_name = wire->name.str() + "$inout.out";
RTLIL::Wire *new_wire = module->wire(wire_name);
if (!new_wire)
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index d3fd91473..951d9c66f 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -193,6 +193,8 @@ YOSYS_NAMESPACE_END
to fix parsing of cells otherwise. (the current cell parser forces a reduce very early to update some
global state.. its a mess) */
[a-zA-Z_$][a-zA-Z0-9_$]*/[ \t\r\n]*:[ \t\r\n]*(assert|assume|cover|restrict)[^a-zA-Z0-9_$\.] {
+ if (!strcmp(yytext, "default"))
+ return TOK_DEFAULT;
frontend_verilog_yylval.string = new std::string(std::string("\\") + yytext);
return TOK_SVA_LABEL;
}
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index d89b2dc88..0fec445fa 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -1021,13 +1021,8 @@ list_of_specparam_assignments:
specparam_assignment:
ignspec_id '=' constant_mintypmax_expression ;
-/*
-pulsestyle_declaration :
- ;
-
-showcancelled_declaration :
- ;
-*/
+ignspec_opt_cond:
+ TOK_IF '(' ignspec_expr ')' | /* empty */;
path_declaration :
simple_path_declaration ';'
@@ -1036,8 +1031,8 @@ path_declaration :
;
simple_path_declaration :
- parallel_path_description '=' path_delay_value |
- full_path_description '=' path_delay_value
+ ignspec_opt_cond parallel_path_description '=' path_delay_value |
+ ignspec_opt_cond full_path_description '=' path_delay_value
;
path_delay_value :
@@ -1047,32 +1042,20 @@ path_delay_value :
;
list_of_path_delay_extra_expressions :
-/*
- t_path_delay_expression
- | trise_path_delay_expression ',' tfall_path_delay_expression
- | trise_path_delay_expression ',' tfall_path_delay_expression ',' tz_path_delay_expression
- | t01_path_delay_expression ',' t10_path_delay_expression ',' t0z_path_delay_expression ','
- tz1_path_delay_expression ',' t1z_path_delay_expression ',' tz0_path_delay_expression
- | t01_path_delay_expression ',' t10_path_delay_expression ',' t0z_path_delay_expression ','
- tz1_path_delay_expression ',' t1z_path_delay_expression ',' tz0_path_delay_expression ','
- t0x_path_delay_expression ',' tx1_path_delay_expression ',' t1x_path_delay_expression ','
- tx0_path_delay_expression ',' txz_path_delay_expression ',' tzx_path_delay_expression
-*/
- ',' path_delay_expression
- | ',' path_delay_expression ',' path_delay_expression
- | ',' path_delay_expression ',' path_delay_expression ','
- path_delay_expression ',' path_delay_expression ',' path_delay_expression
- | ',' path_delay_expression ',' path_delay_expression ','
- path_delay_expression ',' path_delay_expression ',' path_delay_expression ','
- path_delay_expression ',' path_delay_expression ',' path_delay_expression ','
- path_delay_expression ',' path_delay_expression ',' path_delay_expression
- ;
+ ',' path_delay_expression | ',' path_delay_expression list_of_path_delay_extra_expressions;
+
+specify_edge_identifier :
+ TOK_POSEDGE | TOK_NEGEDGE ;
parallel_path_description :
- '(' specify_input_terminal_descriptor opt_polarity_operator '=' '>' specify_output_terminal_descriptor ')' ;
+ '(' specify_input_terminal_descriptor opt_polarity_operator '=' '>' specify_output_terminal_descriptor ')' |
+ '(' specify_edge_identifier specify_input_terminal_descriptor '=' '>' '(' specify_output_terminal_descriptor opt_polarity_operator ':' ignspec_expr ')' ')' |
+ '(' specify_edge_identifier specify_input_terminal_descriptor '=' '>' '(' specify_output_terminal_descriptor TOK_POS_INDEXED ignspec_expr ')' ')' ;
full_path_description :
- '(' list_of_path_inputs '*' '>' list_of_path_outputs ')' ;
+ '(' list_of_path_inputs '*' '>' list_of_path_outputs ')' |
+ '(' specify_edge_identifier list_of_path_inputs '*' '>' '(' list_of_path_outputs opt_polarity_operator ':' ignspec_expr ')' ')' |
+ '(' specify_edge_identifier list_of_path_inputs '*' '>' '(' list_of_path_outputs TOK_POS_INDEXED ignspec_expr ')' ')' ;
// This was broken into 2 rules to solve shift/reduce conflicts
list_of_path_inputs :
@@ -1112,56 +1095,6 @@ system_timing_args :
system_timing_arg |
system_timing_args ',' system_timing_arg ;
-/*
-t_path_delay_expression :
- path_delay_expression;
-
-trise_path_delay_expression :
- path_delay_expression;
-
-tfall_path_delay_expression :
- path_delay_expression;
-
-tz_path_delay_expression :
- path_delay_expression;
-
-t01_path_delay_expression :
- path_delay_expression;
-
-t10_path_delay_expression :
- path_delay_expression;
-
-t0z_path_delay_expression :
- path_delay_expression;
-
-tz1_path_delay_expression :
- path_delay_expression;
-
-t1z_path_delay_expression :
- path_delay_expression;
-
-tz0_path_delay_expression :
- path_delay_expression;
-
-t0x_path_delay_expression :
- path_delay_expression;
-
-tx1_path_delay_expression :
- path_delay_expression;
-
-t1x_path_delay_expression :
- path_delay_expression;
-
-tx0_path_delay_expression :
- path_delay_expression;
-
-txz_path_delay_expression :
- path_delay_expression;
-
-tzx_path_delay_expression :
- path_delay_expression;
-*/
-
path_delay_expression :
ignspec_constant_expression;
diff --git a/kernel/yosys.cc b/kernel/yosys.cc
index f95c0127b..a42a7c0b8 100644
--- a/kernel/yosys.cc
+++ b/kernel/yosys.cc
@@ -1273,6 +1273,10 @@ struct ScriptCmdPass : public Pass {
log("If only one label is specified (without ':') then only the block\n");
log("marked with that label (until the next label) is executed.\n");
log("\n");
+ log("In \"-scriptwire\" mode, the commands on the selected wire(s) will be executed\n");
+ log("in the scope of (and thus, relative to) the wires' owning module(s). This\n");
+ log("'-module' mode can be exited by using the 'cd' command.\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
diff --git a/manual/CHAPTER_Overview.tex b/manual/CHAPTER_Overview.tex
index 1a25c477f..3009bf2c0 100644
--- a/manual/CHAPTER_Overview.tex
+++ b/manual/CHAPTER_Overview.tex
@@ -331,8 +331,9 @@ to update {\tt \textbackslash{}q}.
An RTLIL::Process is a container for zero or more RTLIL::SyncRule objects and
exactly one RTLIL::CaseRule object, which is called the {\it root case}.
-An RTLIL::SyncRule object contains an (optional) synchronization condition
-(signal and edge-type) and zero or more assignments (RTLIL::SigSig).
+An RTLIL::SyncRule object contains an (optional) synchronization condition (signal and edge-type) and zero or
+more assignments (RTLIL::SigSig). The {\tt always} synchronization condition is used to break combinatorial
+loops when a latch should be inferred instead.
An RTLIL::CaseRule is a container for zero or more assignments (RTLIL::SigSig)
and zero or more RTLIL::SwitchRule objects. An RTLIL::SwitchRule objects is a
diff --git a/misc/py_wrap_generator.py b/misc/py_wrap_generator.py
index 9e5727499..66d661fa1 100644
--- a/misc/py_wrap_generator.py
+++ b/misc/py_wrap_generator.py
@@ -779,6 +779,9 @@ class WClass:
#if self.link_type != link_types.pointer:
text += "\n\t\tstatic " + self.name + "* get_py_obj(" + long_name + "* ref)\n\t\t{"
+ text += "\n\t\t\tif(ref == nullptr){"
+ text += "\n\t\t\t\tthrow std::runtime_error(\"" + self.name + " does not exist.\");"
+ text += "\n\t\t\t}"
text += "\n\t\t\t" + self.name + "* ret = (" + self.name + "*)malloc(sizeof(" + self.name + "));"
if self.link_type == link_types.pointer:
text += "\n\t\t\tret->ref_obj = ref;"
diff --git a/passes/memory/memory_dff.cc b/passes/memory/memory_dff.cc
index 5215cce44..32b97f27a 100644
--- a/passes/memory/memory_dff.cc
+++ b/passes/memory/memory_dff.cc
@@ -17,6 +17,7 @@
*
*/
+#include <algorithm>
#include "kernel/yosys.h"
#include "kernel/sigtools.h"
@@ -183,12 +184,12 @@ struct MemoryDffWorker
if (mux_cells_a.count(sig_data) || mux_cells_b.count(sig_data))
{
RTLIL::SigSpec en;
- RTLIL::SigSpec check_q;
+ std::vector<RTLIL::SigSpec> check_q;
do {
bool enable_invert = mux_cells_a.count(sig_data) != 0;
Cell *mux = enable_invert ? mux_cells_a.at(sig_data) : mux_cells_b.at(sig_data);
- check_q = sigmap(mux->getPort(enable_invert ? "\\B" : "\\A"));
+ check_q.push_back(sigmap(mux->getPort(enable_invert ? "\\B" : "\\A")));
sig_data = sigmap(mux->getPort("\\Y"));
en.append(enable_invert ? module->LogicNot(NEW_ID, mux->getPort("\\S")) : mux->getPort("\\S"));
} while (mux_cells_a.count(sig_data) || mux_cells_b.count(sig_data));
@@ -197,7 +198,8 @@ struct MemoryDffWorker
if (sigbit_users_count[bit] > 1)
goto skip_ff_after_read_merging;
- if (find_sig_before_dff(sig_data, clk_data, clk_polarity, true) && clk_data != RTLIL::SigSpec(RTLIL::State::Sx) && sig_data == check_q)
+ if (find_sig_before_dff(sig_data, clk_data, clk_polarity, true) && clk_data != RTLIL::SigSpec(RTLIL::State::Sx) &&
+ std::all_of(check_q.begin(), check_q.end(), [&](const SigSpec &cq) {return cq == sig_data; }))
{
disconnect_dff(sig_data);
cell->setPort("\\CLK", clk_data);
diff --git a/passes/opt/wreduce.cc b/passes/opt/wreduce.cc
index 1fbc41082..f749c8249 100644
--- a/passes/opt/wreduce.cc
+++ b/passes/opt/wreduce.cc
@@ -497,7 +497,7 @@ struct WreducePass : public Pass {
log(" flows that use the 'memory_memx' pass.\n");
log("\n");
log(" -keepdc\n");
- log(" Do not optimize explicit don't-care values.\n");
+ log(" Do not optimize explicit don't-care values on $mux cells.\n");
log("\n");
}
void execute(std::vector<std::string> args, Design *design) YS_OVERRIDE
diff --git a/passes/techmap/muxcover.cc b/passes/techmap/muxcover.cc
index c84cfc39a..d53378a29 100644
--- a/passes/techmap/muxcover.cc
+++ b/passes/techmap/muxcover.cc
@@ -632,10 +632,15 @@ struct MuxcoverPass : public Pass {
log("Cover trees of $_MUX_ cells with $_MUX{4,8,16}_ cells\n");
log("\n");
log(" -mux4[=cost], -mux8[=cost], -mux16[=cost]\n");
- log(" Use the specified types of MUXes (with optional integer costs). If none\n");
- log(" of these options are given, the effect is the same as if all of them are.\n");
- log(" Default costs: $_MUX_ = %d, $_MUX4_ = %d,\n", COST_MUX2, COST_MUX4);
- log(" $_MUX8_ = %d, $_MUX16_ = %d\n", COST_MUX8, COST_MUX16);
+ log(" Cover $_MUX_ trees using the specified types of MUXes (with optional\n");
+ log(" integer costs). If none of these options are given, the effect is the\n");
+ log(" same as if all of them are.\n");
+ log(" Default costs: $_MUX4_ = %d, $_MUX8_ = %d, \n", COST_MUX4, COST_MUX8);
+ log(" $_MUX16_ = %d\n", COST_MUX16);
+ log("\n");
+ log(" -mux2=cost\n");
+ log(" Use the specified cost for $_MUX_ cells when making covering decisions.\n");
+ log(" Default cost: $_MUX_ = %d\n", COST_MUX2);
log("\n");
log(" -dmux=cost\n");
log(" Use the specified cost for $_MUX_ cells used in decoders.\n");
@@ -661,6 +666,7 @@ struct MuxcoverPass : public Pass {
bool nodecode = false;
bool nopartial = false;
int cost_dmux = COST_DMUX;
+ int cost_mux2 = COST_MUX2;
int cost_mux4 = COST_MUX4;
int cost_mux8 = COST_MUX8;
int cost_mux16 = COST_MUX16;
@@ -669,11 +675,15 @@ struct MuxcoverPass : public Pass {
for (argidx = 1; argidx < args.size(); argidx++)
{
const auto &arg = args[argidx];
+ if (arg.size() >= 6 && arg.substr(0,6) == "-mux2=") {
+ cost_mux2 = std::stoi(arg.substr(6));
+ continue;
+ }
if (arg.size() >= 5 && arg.substr(0,5) == "-mux4") {
use_mux4 = true;
if (arg.size() > 5) {
if (arg[5] != '=') break;
- cost_mux4 = atoi(arg.substr(6).c_str());
+ cost_mux4 = std::stoi(arg.substr(6));
}
continue;
}
@@ -681,7 +691,7 @@ struct MuxcoverPass : public Pass {
use_mux8 = true;
if (arg.size() > 5) {
if (arg[5] != '=') break;
- cost_mux8 = atoi(arg.substr(6).c_str());
+ cost_mux8 = std::stoi(arg.substr(6));
}
continue;
}
@@ -689,12 +699,12 @@ struct MuxcoverPass : public Pass {
use_mux16 = true;
if (arg.size() > 6) {
if (arg[6] != '=') break;
- cost_mux16 = atoi(arg.substr(7).c_str());
+ cost_mux16 = std::stoi(arg.substr(7));
}
continue;
}
if (arg.size() >= 6 && arg.substr(0,6) == "-dmux=") {
- cost_dmux = atoi(arg.substr(6).c_str());
+ cost_dmux = std::stoi(arg.substr(6));
continue;
}
if (arg == "-nodecode") {
@@ -722,6 +732,7 @@ struct MuxcoverPass : public Pass {
worker.use_mux8 = use_mux8;
worker.use_mux16 = use_mux16;
worker.cost_dmux = cost_dmux;
+ worker.cost_mux2 = cost_mux2;
worker.cost_mux4 = cost_mux4;
worker.cost_mux8 = cost_mux8;
worker.cost_mux16 = cost_mux16;
diff --git a/techlibs/common/synth.cc b/techlibs/common/synth.cc
index 555de9fba..af70cc498 100644
--- a/techlibs/common/synth.cc
+++ b/techlibs/common/synth.cc
@@ -78,6 +78,9 @@ struct SynthPass : public ScriptPass
log(" -abc9\n");
log(" use new ABC9 flow (EXPERIMENTAL)\n");
log("\n");
+ log(" -keepdc\n");
+ log(" do not optimize explicit don't-care values on $mux cells.\n");
+ log("\n");
log("\n");
log("The following commands are executed by this synthesis command:\n");
help_script();
@@ -85,7 +88,7 @@ struct SynthPass : public ScriptPass
}
string top_module, fsm_opts, memory_opts, abc;
- bool autotop, flatten, noalumacc, nofsm, noabc, noshare;
+ bool autotop, flatten, noalumacc, nofsm, noabc, noshare, keepdc;
int lut;
void clear_flags() YS_OVERRIDE
@@ -102,6 +105,7 @@ struct SynthPass : public ScriptPass
noabc = false;
noshare = false;
abc = "abc";
+ keepdc = false;
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
@@ -167,6 +171,10 @@ struct SynthPass : public ScriptPass
abc = "abc9";
continue;
}
+ if (args[argidx] == "-keepdc") {
+ keepdc = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
@@ -211,7 +219,10 @@ struct SynthPass : public ScriptPass
run("opt_clean");
run("check");
run("opt");
- run("wreduce");
+ if (help_mode)
+ run("wreduce [-keepdc]");
+ else
+ run("wreduce" + std::string(keepdc ? " -keepdc" : ""));
run("peepopt");
run("opt_clean");
if (help_mode)
diff --git a/techlibs/intel/synth_intel.cc b/techlibs/intel/synth_intel.cc
index 639cba2c2..09c9ba3af 100644
--- a/techlibs/intel/synth_intel.cc
+++ b/techlibs/intel/synth_intel.cc
@@ -48,6 +48,8 @@ struct SynthIntelPass : public ScriptPass {
log(" -vqm <file>\n");
log(" write the design to the specified Verilog Quartus Mapping File. Writing of an\n");
log(" output file is omitted if this parameter is not specified.\n");
+ log(" Note that this backend has not been tested and is likely incompatible\n");
+ log(" with recent versions of Quartus.\n");
log("\n");
log(" -vpr <file>\n");
log(" write BLIF files for VPR flow experiments. The synthesized BLIF output file is not\n");
@@ -108,6 +110,7 @@ struct SynthIntelPass : public ScriptPass {
}
if (args[argidx] == "-vqm" && argidx + 1 < args.size()) {
vout_file = args[++argidx];
+ log_warning("The Quartus backend has not been tested recently and is likely incompatible with modern versions of Quartus.\n");
continue;
}
if (args[argidx] == "-vpr" && argidx + 1 < args.size()) {
diff --git a/tests/memories/read_two_mux.v b/tests/memories/read_two_mux.v
new file mode 100644
index 000000000..4f2e7e1cd
--- /dev/null
+++ b/tests/memories/read_two_mux.v
@@ -0,0 +1,16 @@
+// expect-wr-ports 1
+// expect-rd-ports 1
+// expect-no-rd-clk
+
+module top(input clk, input we, re, reset, input [7:0] addr, wdata, output reg [7:0] rdata);
+
+reg [7:0] bram[0:255];
+(* keep *) reg dummy;
+
+always @(posedge clk) begin
+ rdata <= re ? (reset ? 8'b0 : bram[addr]) : rdata;
+ if (we)
+ bram[addr] <= wdata;
+end
+
+endmodule
diff --git a/tests/memories/run-test.sh b/tests/memories/run-test.sh
index 76acaa9cd..8d1a8b413 100755
--- a/tests/memories/run-test.sh
+++ b/tests/memories/run-test.sh
@@ -31,6 +31,10 @@ for f in `egrep -l 'expect-(wr-ports|rd-ports|rd-clk)' *.v`; do
grep -q "connect \\\\RD_CLK \\$(gawk '/expect-rd-clk/ { print $3; }' $f)\$" ${f%.v}.dmp ||
{ echo " ERROR: Unexpected read clock."; false; }
fi
+ if grep -q expect-no-rd-clk $f; then
+ grep -q "connect \\\\RD_CLK 1'x\$" ${f%.v}.dmp ||
+ { echo " ERROR: Expected no read clock."; false; }
+ fi
echo " ok."
done
diff --git a/tests/various/abc9.v b/tests/various/abc9.v
index 8271cd249..a08b613a8 100644
--- a/tests/various/abc9.v
+++ b/tests/various/abc9.v
@@ -3,3 +3,7 @@ initial o = 1'b0;
always @*
o <= ~o;
endmodule
+
+module abc9_test028(input i, output o);
+unknown u(~i, o);
+endmodule
diff --git a/tests/various/abc9.ys b/tests/various/abc9.ys
index 922f7005d..a84b637d9 100644
--- a/tests/various/abc9.ys
+++ b/tests/various/abc9.ys
@@ -1,4 +1,6 @@
read_verilog abc9.v
+design -save read
+hierarchy -top abc9_test027
proc
design -save gold
@@ -12,3 +14,11 @@ design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
+design -load read
+hierarchy -top abc9_test028
+proc
+
+abc9 -lut 4
+select -assert-count 1 t:$lut r:LUT=1 r:WIDTH=1 %i %i
+select -assert-count 1 t:unknown
+select -assert-none t:$lut t:unknown %% t: %D
diff --git a/tests/various/specify.v b/tests/various/specify.v
index afc421da8..5d44d78f7 100644
--- a/tests/various/specify.v
+++ b/tests/various/specify.v
@@ -7,9 +7,11 @@ module test (
if (EN) Q <= D;
specify
- if (EN) (CLK *> (Q : D)) = (1, 2:3:4);
+`ifndef SKIP_UNSUPPORTED_IGN_PARSER_CONSTRUCTS
+ if (EN) (posedge CLK *> (Q : D)) = (1, 2:3:4);
$setup(D, posedge CLK &&& EN, 5);
$hold(posedge CLK, D &&& EN, 6);
+`endif
endspecify
endmodule
@@ -28,3 +30,10 @@ module test2 (
(B => Q) = 1.5;
endspecify
endmodule
+
+module issue01144(input clk, d, output q);
+specify
+ (posedge clk => (q +: d)) = (3,1);
+ (posedge clk *> (q +: d)) = (3,1);
+endspecify
+endmodule
diff --git a/tests/various/specify.ys b/tests/various/specify.ys
index a5ca07219..00597e1e2 100644
--- a/tests/various/specify.ys
+++ b/tests/various/specify.ys
@@ -54,3 +54,5 @@ equiv_struct
equiv_induct -seq 5
equiv_status -assert
design -reset
+
+read_verilog -DSKIP_UNSUPPORTED_IGN_PARSER_CONSTRUCTS specify.v
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-08 10:06:39 +0000