Merge 1cfba3c into 4e7e0da

azure-pipelines.yml

@@ -27,10 +27,9 @@ jobs:
       export LDFLAGS="-L/usr/local/opt/bison/lib"
       mkdir -p build 
       cd build
-      cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON -DILANG_BUILD_INVSYN=OFF
+      cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON
       cmake --build .
-      cmake --build . --target install 
-      cmake --build . --target test
+      ./test/unit_tests
     displayName: 'build'
 
 - job: macOS_Mojave
@@ -53,10 +52,9 @@ jobs:
       export LDFLAGS="-L/usr/local/opt/bison/lib"
       mkdir -p build 
       cd build
-      cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON -DILANG_BUILD_INVSYN=OFF
+      cmake .. -DCMAKE_BUILD_TYPE=Release -DBoost_NO_BOOST_CMAKE=ON
       cmake --build .
-      cmake --build . --target install 
-      cmake --build . --target test
+      ./test/unit_tests
     displayName: 'build'
 
 - job: Linux

extern/smt-parser/include/smtparser/smtlib2abstractparser.h

@@ -38,5 +38,6 @@ void smtlib2_abstract_parser_init(smtlib2_abstract_parser *p,
                                   smtlib2_context ctx);
 void smtlib2_abstract_parser_deinit(smtlib2_abstract_parser *p);
 void smtlib2_abstract_parser_parse(smtlib2_abstract_parser *p, FILE *src);
+void smtlib2_abstract_parser_parse_string(smtlib2_abstract_parser *p, const char * str);
 
 #endif /* SMTLIB2ABSTRACTPARSER_H_INCLUDED */

extern/smt-parser/src/smtlib2abstractparser.c

@@ -129,6 +129,36 @@ void smtlib2_abstract_parser_parse(smtlib2_abstract_parser *p, FILE *src)
 }
 
 
+void smtlib2_abstract_parser_parse_string(smtlib2_abstract_parser *p, const char * str)
+{
+    smtlib2_charbuf *buf;
+    smtlib2_fstream *stream;
+    smtlib2_scanner *scanner;
+
+    buf = smtlib2_charbuf_new();
+    smtlib2_charbuf_push_str(buf, str);
+    stream = smtlib2_sstream_new(buf);
+    scanner = smtlib2_scanner_new((smtlib2_stream *)stream);
+
+    smtlib2_abstract_parser_reset_response(p);
+
+    while (!smtlib2_stream_eof((smtlib2_stream *)stream)) {
+        smtlib2_parse(scanner, SMTLIB2_PARSER_INTERFACE(p));
+        if (p->exiting_) {
+            break;
+        }
+        if (!smtlib2_stream_eof((smtlib2_stream *)stream)) {
+            smtlib2_abstract_parser_print_response(p);
+            smtlib2_abstract_parser_reset_response(p);
+        }
+    }
+
+    smtlib2_scanner_delete(scanner);
+    smtlib2_fstream_delete(stream);
+    smtlib2_charbuf_delete(buf);
+}
+
+
 void smtlib2_abstract_parser_set_logic(smtlib2_parser_interface *p,
                                        const char *logic)
 {

include/ilang/mcm/ast_helper.h

@@ -10,6 +10,7 @@
 #include <utility>
 
 #include "ilang/ila/instr_lvl_abs.h"
+#include "ilang/vtarget-out/directive.h"
 
 /// \namespace ilang
 namespace ilang {
@@ -74,6 +75,10 @@ class NestedMemAddrDataAvoider {
   bool InAddrOrData;
 }; // class NestedMemAddrDataAvoider
 
+/// \brief Function to deal with Ite(c, v, apply(__unknown__) );
+bool getIteUnknownCondVal(const ExprPtr & e, ExprPtr & c, ExprPtr & v);
+
+
 /// \brief Class of traversing to find the application of functions in an AST
 class FunctionApplicationFinder {
 protected:

include/ilang/verilog-out/verilog_gen.h

@@ -127,6 +127,15 @@ class VerilogGeneratorBase {
   }; // struct function_app_t
   typedef std::vector<function_app_t> function_app_vec_t;
 
+  /// Type of ite update unknown 
+  struct state_update_unknown {
+    /// the condition
+    const vlg_name_t condition;
+    // you don't need the value
+    state_update_unknown(const vlg_name_t & c) : condition(c) {}
+  }; // struct state_update_unknown
+  typedef std::map<std::string, state_update_unknown> state_update_ite_unknown_map_t;
+
   /// Type for caching the generated expressions.
   typedef std::unordered_map<const ExprPtr, vlg_name_t, VerilogGenHash> ExprMap;
   /// Type for cacheing the constant
@@ -153,22 +162,24 @@ class VerilogGeneratorBase {
     /// whether to expand the memory and connect everything to the outside
     /// cannot be true the same time as extMem
     bool expand_mem;
+    /// whether to collect the ite(c, v, unknown) thing
+    bool collect_ite_unknown_update;
 
     /// Constructor, set default value, ExternalMem : false, function: internal
     /// module
     VlgGenConfig( // provide the default settings
         bool ExternalMem = true, funcOption funcOpt = funcOption::Internal,
         bool gen_start = false, bool pass_name = false, bool rand_init = false,
-        bool ExpandMem = false)
+        bool ExpandMem = false, bool CollectIteUnknownUpdate = false)
         : extMem(ExternalMem), fcOpt(funcOpt), start_signal(gen_start),
           pass_node_name(pass_name), reg_random_init(rand_init),
-          expand_mem(ExpandMem) {}
+          expand_mem(ExpandMem), collect_ite_unknown_update(CollectIteUnknownUpdate) {}
     /// Overwrite configuration, used by vtarget gen
     VlgGenConfig(const VlgGenConfig& c, bool ExternalMem, funcOption funcOpt,
-                 bool gen_start, bool rand_init, bool ExpandMem)
+                 bool gen_start, bool rand_init, bool ExpandMem, bool CollectIteUnknownUpdate)
         : extMem(ExternalMem), fcOpt(funcOpt), start_signal(gen_start),
           pass_node_name(c.pass_node_name), reg_random_init(rand_init),
-          expand_mem(ExpandMem) {}
+          expand_mem(ExpandMem), collect_ite_unknown_update(CollectIteUnknownUpdate) {}
     // set other fields if there are such need (?)
   }; // end of struct VlgGenConfig
 
@@ -268,7 +279,8 @@ class VerilogGeneratorBase {
   std::map<std::string, std::map<unsigned, wport_t>> ila_wports;
   /// a collection of all function application
   function_app_vec_t ila_func_app;
-
+  /// a collection of all state update ite unknown
+  state_update_ite_unknown_map_t state_update_ite_unknown;
   // Annotations
   memory_export_annotation_t memory_export_annotation;
 

include/ilang/vtarget-out/directive.h

@@ -169,7 +169,10 @@ class StateMappingDirectiveRecorder {
   static bool isSpecialStateDir(const std::string& c);
   /// a function to determine if a state map refstr is special directie (**???)
   static bool isSpecialStateDirMem(const std::string& c);
-
+  /// a function to determine if a function name is an unknown special directive
+  static bool isSpecialUnknownFunctionName(const std::string &funcname);
+  /// a function to determine if a function (no arg) is an unknown special directive
+  static bool isSpecialUnknownFunction(const FuncPtr &func_ptr);
 }; // class StateMappingDirectiveRecorder
 
 }; // namespace ilang

include/ilang/vtarget-out/vtarget_gen.h

@@ -63,6 +63,12 @@ class VlgVerifTgtGenBase {
     /// Does not insert assertions of variable mapping
     /// if an instruction does not update that var
     bool OnlyCheckInstUpdatedVars; // true
+    /// A shortcut for SetUpdate(s, Ite(c, v, __unknown__() ))
+    /// will only gnerate map like : ( ila.c => ila.v == vlg.v )
+    /// In this case, you don't need to deal with unknown in func map
+    /// nor do you need to create a special refinement map
+    /// function has to be defined as __unknown__X
+    bool IteUnknownAutoIgnore; // false
     /// whether to remove the extra issue cycle and starts from reset
     bool VerificationSettingAvoidIssueStage;
     /// Configure the behavior of INV target, if false,
@@ -207,6 +213,7 @@ class VlgVerifTgtGenBase {
     _vtg_config()
         : target_select(BOTH), CheckThisInstructionOnly(""),
           InstructionNoReset(true), OnlyCheckInstUpdatedVars(true),
+          IteUnknownAutoIgnore(false),
           VerificationSettingAvoidIssueStage(false),
           ValidateSynthesizedInvariant(ALL),
 

src/mcm/ast_helper.cc

@@ -169,6 +169,44 @@ FunctionApplicationFinder::GetReferredFunc() const {
   return _func_refs;
 }
 
+
+
+bool getIteUnknownCondVal(const ExprPtr & e, ExprPtr & c, ExprPtr & v) {
+  if (!e->is_op())
+    return false;
+  std::shared_ptr<ExprOp> eop = std::dynamic_pointer_cast<ExprOp>(e);
+  if (!(eop && eop->op_name() == "ITE"))
+    return false;
+  ILA_ASSERT(eop->arg_num() == 3);
+  { // test arg 1
+    std::shared_ptr<ExprOp> arg1 = std::dynamic_pointer_cast<ExprOp>(eop->arg(1));
+    if ( (arg1 && arg1->op_name() == "APP") ) {
+      std::shared_ptr<ExprOpAppFunc> apply_op_arg1 =
+        std::dynamic_pointer_cast<ExprOpAppFunc>(arg1);
+      if ( StateMappingDirectiveRecorder::isSpecialUnknownFunction(apply_op_arg1->func())) {
+        c = eop->arg(0);
+        v = eop->arg(2);
+        return true;
+      }
+    }
+  } // end test arg 1
+
+  { // test arg 2
+    std::shared_ptr<ExprOp> arg2 = std::dynamic_pointer_cast<ExprOp>(eop->arg(2));
+    if ( (arg2 && arg2->op_name() == "APP") ) {
+      std::shared_ptr<ExprOpAppFunc> apply_op_arg2 =
+        std::dynamic_pointer_cast<ExprOpAppFunc>(arg2);
+      if ( StateMappingDirectiveRecorder::isSpecialUnknownFunction(apply_op_arg2->func())) {
+        c = eop->arg(0);
+        v = eop->arg(1);
+        return true;
+      }
+    }
+  } // end test arg 2
+
+  return false;
+}
+
 /******************************************************************************/
 // Helper Class: NestedMemAddrDataAvoider
 /******************************************************************************/

src/smt-inout/chc_inv_in.cc

@@ -911,7 +911,7 @@ void SmtlibInvariantParser::ParseSmtResultFromString(const std::string& text) {
   ILA_ASSERT(buffer[len - 1] == '\0');
   buffer[len - 1] = '\0'; // to make static analysis happy
 
-  std::FILE* fp = fmemopen((void*)buffer, len * sizeof(char), "r");
+  //std::FILE* fp = fmemopen((void*)buffer, len * sizeof(char), "r");
 #if 0
 #if defined(__linux__) 
   std::FILE* fp = fmemopen((void*)buffer, len * sizeof(char), "r");
@@ -922,11 +922,11 @@ void SmtlibInvariantParser::ParseSmtResultFromString(const std::string& text) {
 #endif
 #endif //  
 
-  ILA_NOT_NULL(fp);
-
-  smtlib2_abstract_parser_parse(&(parser_wrapper->parser), fp);
+  //ILA_NOT_NULL(fp);
+  smtlib2_abstract_parser_parse_string(&(parser_wrapper->parser), buffer);
+  //smtlib2_abstract_parser_parse(&(parser_wrapper->parser), fp);
 
-  fclose(fp);
+  //fclose(fp);
   delete[] buffer;
 }
 

src/verilog-out/verilog_gen.cc

@@ -13,6 +13,7 @@
 #include <ilang/util/container_shortcut.h>
 #include <ilang/util/log.h>
 #include <ilang/util/str_util.h>
+#include <ilang/mcm/ast_helper.h>
 
 namespace ilang {
 
@@ -1378,6 +1379,21 @@ void VerilogGenerator::ExportTopLevelInstr(const InstrPtr& instr_ptr_) {
       vlg_name_t result = getVlgFromExpr(update);
       add_ite_stmt(decodeName, sanitizeName(var) + " <= " + result, "");
     } // else
+
+    ExprPtr c, v;
+    if (cfg_.collect_ite_unknown_update && getIteUnknownCondVal(update, c, v)) {
+      auto original_cond_sig = getVlgFromExpr(c);
+      auto sig_name = "__ite_ukn_cond_" + original_cond_sig;
+      auto reg_name = "__ite_ukn_cond_reg_" + original_cond_sig;
+      state_update_ite_unknown.insert(
+        std::make_pair(var->name().str(),
+          state_update_unknown(sig_name)));
+      add_output(sig_name, 1);
+      add_wire(sig_name, 1);
+      add_assign_stmt(sig_name, reg_name);
+      add_ite_stmt(decodeName, reg_name + " <= " + original_cond_sig, "");
+    }
+
   }   // for (size_t idx = 0;  ...
 
   // Func Defs

src/vtarget-out/directive.cc

@@ -574,4 +574,23 @@ bool StateMappingDirectiveRecorder::isSpecialStateDirMem(const std::string& c) {
   return IntefaceDirectiveRecorder::beginsWith(c, "**MEM**");
 }
 
+bool StateMappingDirectiveRecorder::isSpecialUnknownFunctionName(const std::string &funcname) {
+  if (funcname.length() < 11)
+    return false;
+  if (!StrStartsWith(funcname, "__unknown__"))
+    return false;
+  if (funcname == "__unknown__")
+    return true;
+  for (size_t idx = 11; idx < funcname.length(); ++ idx)
+    if (!isdigit(funcname.at(idx)))
+      return false;
+  return true;
+}
+
+bool StateMappingDirectiveRecorder::isSpecialUnknownFunction(const FuncPtr &func_ptr) {
+  if (func_ptr->arg_num() > 0)
+    return false;
+  return isSpecialUnknownFunctionName(func_ptr->name().str());
+}
+
 } // namespace ilang

src/vtarget-out/inv-syn/vtarget_gen_inv_chc.cc

@@ -21,6 +21,9 @@ namespace ilang {
 #define VLG_TRUE "`true"
 #define VLG_FALSE "`false"
 
+// hierarchy --> opt may not be useful
+// mux undef may be useful?
+
 // initialize templates
 static std::string chcGenerateSmtScript_wo_Array = R"***(
 hierarchy -check

src/vtarget-out/single_target.cc

@@ -52,7 +52,8 @@ VlgSglTgtGen::VlgSglTgtGen(
                                              funcOption::External, // function
                                          false,  // no start signal
                                          false,  // no rand init
-                                         false), // no expand memory
+                                         false,  // no expand memory
+                                         false), // no collect ITE unknown
           wrapper_name),
       // use given, except for core options
       vlg_ila(VerilogGeneratorBase::VlgGenConfig(
@@ -63,7 +64,8 @@ VlgSglTgtGen::VlgSglTgtGen(
               .extMem, // this depends on the given configuration (default case)
           VerilogGeneratorBase::VlgGenConfig::funcOption::External, true,
           true, // rand init
-          true  // for internal should always expand (probe) memory
+          true, // for internal should always expand (probe) memory
+          vtg_config.IteUnknownAutoIgnore // may collect depends on configuration
           )),
       // interface mapping directive
       // -------- CONTROLLING THE RESET CONNECTION ------------- //
@@ -311,6 +313,9 @@ void VlgSglTgtGen::ConstructWrapper_add_varmap_assertions() {
     if (_instr_ptr->update(sname)) {
       FunctionApplicationFinder func_app_finder(_instr_ptr->update(sname));
       for (auto&& func_ptr : func_app_finder.GetReferredFunc()) {
+        // handle the IteUnknown function case
+        if (_vtg_config.IteUnknownAutoIgnore && _sdr.isSpecialUnknownFunction(func_ptr))
+          continue;
         ILA_ERROR_IF(!(IN("functions", rf_vmap) &&
                        rf_vmap["functions"].is_object() &&
                        IN(func_ptr->name().str(), rf_vmap["functions"])))
@@ -323,6 +328,11 @@ void VlgSglTgtGen::ConstructWrapper_add_varmap_assertions() {
     // ISSUE ==> vmap
     std::string precondition =
         has_flush ? "(~ __ENDFLUSH__) || " : "(~ __IEND__) || ";
+
+    if (IN(sname, vlg_ila.state_update_ite_unknown)) {
+      auto pos = vlg_ila.state_update_ite_unknown.find(sname);
+      precondition += "(~ " + pos->second.condition +") ||";
+    }
 
     std::string problem_name = "variable_map_assert";
     if (_vtg_config.PerVariableProblemCosa &&

src/vtarget-out/single_target_connect.cc

@@ -72,6 +72,18 @@ std::string VlgSglTgtGen::ConstructWrapper_get_ila_module_inst() {
   auto retStr = vlg_ila.moduleName + " " + _ila_mod_inst_name + " (\n";
 
   std::set<std::string> func_port_skip_set;
+
+  // ite ( unknown) also use this port
+  for (auto&& sname_cond_pair  : vlg_ila.state_update_ite_unknown) {
+    const auto & port_name = sname_cond_pair.second.condition;
+    func_port_skip_set.insert( port_name );
+    port_connected.insert( port_name );
+    vlg_wrapper.add_wire(port_name, 1, true);
+    vlg_wrapper.add_output(port_name, 1);
+
+    retStr += "   ." + port_name + "(" + port_name + "),\n";
+  }
+
   for (auto&& func_app : vlg_ila.ila_func_app) {
     func_port_skip_set.insert(func_app.result.first);
     port_connected.insert(func_app.result.first);

src/vtarget-out/single_target_misc.cc

@@ -109,8 +109,13 @@ void VlgSglTgtGen::ConstructWrapper_add_uf_constraints() {
   // convert vlg_ila.ila_func_app to  name->list of func_app
   std::map<std::string, VerilogGeneratorBase::function_app_vec_t>
       name_to_fnapp_vec;
-  for (auto&& func_app : vlg_ila.ila_func_app)
+  for (auto&& func_app : vlg_ila.ila_func_app) {
+    if (_vtg_config.IteUnknownAutoIgnore) {
+      if ( func_app.args.empty() && _sdr.isSpecialUnknownFunctionName(func_app.func_name) )
+        continue;
+    }
     name_to_fnapp_vec[func_app.func_name].push_back(func_app);
+  }
 
   for (auto&& it : fm.items()) {
     const auto& funcName = it.key();