From 979347999f72591b5536e58110cfd491edccc937 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcelina=20Ko=C5=9Bcielnicka?= Date: Tue, 23 Feb 2021 12:06:21 +0100 Subject: btor, smt2, smv: Add a hint on how to deal with funny FF types. --- backends/btor/btor.cc | 15 ++++++++++++++- backends/smt2/smt2.cc | 12 ++++++++++++ backends/smv/smv.cc | 18 ++++++++++++++++-- 3 files changed, 42 insertions(+), 3 deletions(-) (limited to 'backends') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 639c6f129..692452aad 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -860,7 +860,20 @@ struct BtorWorker goto okay; } - log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell)); + if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) { + log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_btor`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_btor`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_btor`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + log_error("Unsupported cell type %s for cell %s.%s.\n", + log_id(cell->type), log_id(module), log_id(cell)); okay: btorf_pop(log_id(cell)); diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a185fdd74..8be9e05f1 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -855,6 +855,18 @@ struct Smt2Worker return; } + if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) { + log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smt2`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smt2`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smt2`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } log_error("Unsupported cell type %s for cell %s.%s.\n", log_id(cell->type), log_id(module), log_id(cell)); } diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc index 4e5c6050d..e41582fea 100644 --- a/backends/smv/smv.cc +++ b/backends/smv/smv.cc @@ -573,8 +573,22 @@ struct SmvWorker continue; } - if (cell->type[0] == '$') - log_error("Found currently unsupported cell type %s (%s.%s).\n", log_id(cell->type), log_id(module), log_id(cell)); + if (cell->type[0] == '$') { + if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) { + log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smv`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smv`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") { + log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smv`.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } + log_error("Unsupported cell type %s for cell %s.%s.\n", + log_id(cell->type), log_id(module), log_id(cell)); + } // f << stringf(" %s : %s;\n", cid(cell->name), cid(cell->type)); -- cgit v1.2.3