aqed export io signal; usage see test/t_aqed_support.cc

include/ilang/aqed-out/aqed_out.h

@@ -0,0 +1,46 @@
+/// \file Header for generating information to support
+/// AQED
+// --- Hongce Zhang (hongcez@princeton.edu)
+
+#ifndef ILANG_AQED_OUT_AQED_OUT_H__
+#define ILANG_AQED_OUT_AQED_OUT_H__
+
+#include <ilang/ila/instr_lvl_abs.h>
+
+namespace ilang {
+
+/// \brief the interface class for info generator
+/// must be instantiated through the factory
+/// just to hide the implementation details
+class AQedInfoGenerator {
+  typedef std::shared_ptr<AQedInfoGenerator> AQedInfoGeneratorPtr;
+public:
+  // --------------------- CONSTRUCTOR ---------------------------- //
+  AQedInfoGenerator();
+  // --------------------- DESTRUCTOR ---------------------------- //
+  virtual ~AQedInfoGenerator();
+
+  // --------------------- MEMBER FUNCTIONS ---------------------------- //
+  /// Export the top-level io in  a file
+  /// \param[in] filename to be exported
+  virtual void ExportVerilogTopLevelIOInfo(const std::string& fname) = 0;
+  /// Export the decode function and etc
+  /// \param[in] filename to be exported
+  virtual void ExportInstructionAndDecode(const std::string& filename) = 0;
+  /// Export the signal references
+  /// \param[in] filename to be exported
+  virtual void ExportExtraSignalReferenced(const std::string& fname) = 0;
+  /// the factory to create such an object
+  static AQedInfoGeneratorPtr Create(
+    const std::vector<std::string>& implementation_include_path,
+    const std::vector<std::string>& implementation_srcs,
+    const std::string& implementation_top_module,
+    const std::string& refinement_variable_mapping,
+    const std::string& refinement_conditions,
+    const InstrLvlAbsCnstPtr& ila_ptr_);
+}; // class AQedInfoGeneratorBase
+
+}; // namespace ilang
+
+
+#endif // ILANG_AQED_OUT_AQED_OUT_H__

include/ilang/aqed-out/aqed_out_impl.h

@@ -0,0 +1,101 @@
+/// \file Header for generating information to support
+/// AQED --- the implementation, not to be exposed
+// --- Hongce Zhang (hongcez@princeton.edu)
+
+#ifndef ILANG_AQED_OUT_AQED_OUT_IMPL_H__
+#define ILANG_AQED_OUT_AQED_OUT_IMPL_H__
+
+#include "nlohmann/json.hpp"
+
+#include <ilang/aqed-out/aqed_out.h>
+#include <ilang/aqed-out/aqed_vlog_out.h>
+#include <ilang/verilog-in/verilog_analysis_wrapper.h>
+#include <ilang/vtarget-out/supplementary_info.h>
+#include <ilang/vtarget-out/var_extract.h>
+#include <ilang/vtarget-out/vtarget_gen.h>
+
+
+namespace ilang {
+
+
+/// \brief the base class for info generator
+/// will use a lot of other headers like
+/// the verilog parser
+class AQedInfoGeneratorImpl : public AQedInfoGenerator {
+public:
+  /// Type of record of extra info of a signal
+  using ex_info_t = VlgVerifTgtGenBase::ex_info_t;
+protected:
+  /// The pointer to the instruction that is going to export
+  const InstrLvlAbsCnstPtr& _ila_ptr;
+  /// implementation top module name
+  const std::string _vlg_impl_top_name;
+  /// The name of verilog top module instance in the wrapper
+  std::string _vlg_mod_inst_name;
+  /// The name of ila-verilog top module instance in the wrapper
+  std::string _ila_mod_inst_name;
+  /// A pointer to create verilog analyzer
+  VerilogInfo* vlg_info_ptr; // in case we want to share it
+  /// store the vmap info
+  nlohmann::json rf_vmap;
+  /// store the condition
+  nlohmann::json rf_cond;
+  /// The supplementary information
+  VlgTgtSupplementaryInfo supplementary_info;
+  /// Var extractor
+  VarExtractor _vext;
+  /// record all the referred vlg names, so you can add (*keep*) if needed
+  std::map<std::string, ex_info_t> _all_referred_vlg_names;
+  /// in case we reference out variables
+  /// vlgname, mod input name, width 
+  std::vector<std::tuple<std::string, std::string, unsigned>> outer_var_reference;
+
+public:
+  // --------------------- CONSTRUCTOR ---------------------------- //
+  AQedInfoGeneratorImpl(
+    const std::vector<std::string>& implementation_include_path,
+    const std::vector<std::string>& implementation_srcs,
+    const std::string& implementation_top_module,
+    const std::string& refinement_variable_mapping,
+    const std::string& refinement_conditions,
+    const InstrLvlAbsCnstPtr& ila_ptr
+  );
+  // --------------------- DESTRUCTOR ---------------------------- //
+  virtual ~AQedInfoGeneratorImpl();
+  /// Return true if it is in bad state
+  bool in_bad_state(void) const { return _bad_state; }
+  /// Export the top-level io in  a file
+  virtual void ExportVerilogTopLevelIOInfo(const std::string& fname) override;
+  /// Export the decode function and etc
+  virtual void ExportInstructionAndDecode(const std::string& filename) override;
+  /// Export the signal references
+  virtual void ExportExtraSignalReferenced(const std::string& fname) override;
+
+protected:
+  /// If it is bad state, return true and display a message
+  bool bad_state_return(void);
+  /// load json from a file name to the given j
+  void load_json(const std::string& fname, nlohmann::json& j);
+  /// Get instance name from rfmap
+  void set_module_instantiation_name();
+  // To check if we should precede
+  std::string
+  CheckNames(
+    const VarExtractor::token& t, 
+    const std::set<std::string>& ns,
+    bool& has_ila_input_state_in_ns, bool& has_ila_input_state_outof_ns );
+  /// To replace a string of expression
+  std::string ModifyCondExprAndRecordVlgName(const VarExtractor::token& t,
+    const std::set<std::string>& top_level_vlg_input_names);
+  /// Add wires to vlg module
+  void RegisterExtraVlgReferenceWire(VerilogGeneratorBase& vlg_gen);
+
+private:
+  /// If it is in a bad state
+  bool _bad_state;
+
+}; // // 
+
+}; // namespace ilang
+
+#endif // ILANG_AQED_OUT_AQED_OUT_IMPL_H__

include/ilang/aqed-out/aqed_vlog_out.h

@@ -0,0 +1,110 @@
+/// \file Header for generating decode for each instruction
+// --- Hongce Zhang (hongcez@princeton.edu)
+
+#ifndef ILANG_AQED_OUT_VLOG_OUT_H__
+#define ILANG_AQED_OUT_VLOG_OUT_H__
+
+#include <ilang/verilog-out/verilog_gen.h>
+
+namespace ilang {
+
+/// \brief Class of Verilog Decode AQed Generator
+class VerilogDecodeForAQedGenerator : public VerilogGenerator {
+public:
+  // --------------------- TYPE DEFINITIONS ---------------------------- //
+  /// let the test class use this module
+  friend class TestVerilogExport;
+  /// Type of Verilog id names'
+  using vlg_name_t = VerilogGenerator::vlg_name_t;
+  /// Type of Verilog statement
+  using vlg_stmt_t = VerilogGenerator::vlg_stmt_t;
+  /// Type of Verilog address
+  using vlg_addr_t = VerilogGenerator::vlg_addr_t;
+  /// Type of Verilog data
+  using vlg_data_t = VerilogGenerator::vlg_data_t;
+  /// Type of Verilog statements (a vector)
+  using vlg_stmts_t = VerilogGenerator::vlg_stmts_t;
+  /// Type of Verilog names (a vector)
+  using vlg_names_t = VerilogGenerator::vlg_names_t;
+  /// Type of Verilog signal, name & bw
+  using vlg_sig_t = VerilogGenerator::vlg_sig_t;
+  /// Type of Verilog signals (a vector)
+  using vlg_sigs_t = VerilogGenerator::vlg_sigs_t;
+  /// Type of a map: name -> need to add keep?
+  using vlg_sig_keep_t = VerilogGenerator::vlg_sig_keep_t;
+  /// Type of set of Verilog signals
+  using vlg_sigs_set_t = VerilogGenerator::vlg_sigs_set_t;
+  /// Type of Verilog ITEs (IN sequential block)
+  using vlg_ite_stmt_t = VerilogGenerator::vlg_ite_stmt_t;
+  /// Type of Verilog ITEs statements
+  using vlg_ite_stmts_t = VerilogGenerator::vlg_ite_stmts_t;
+  /// Type of the memorys that are going to be created
+  using vlg_mem_t = VerilogGenerator::vlg_mem_t;
+  /// Type of collection of memorys
+  using vlg_mems_rec_t = VerilogGenerator::vlg_mems_rec_t;
+  /// This is type of an individual write.
+  using mem_write_entry_t = VerilogGenerator::mem_write_entry_t;
+  /// This is type of a list of writes.
+  using mem_write_entry_list_t = VerilogGenerator::mem_write_entry_list_t;
+  /// Type of a stack of writes use in visitMemNodes
+  using mem_write_entry_list_stack_t =
+      VerilogGenerator::mem_write_entry_list_stack_t;
+  /// This is the write and its associated condition.
+  using mem_write_t = VerilogGenerator::mem_write_t;
+  /// List of writes w. associated conditions.
+  using mem_write_list_t = VerilogGenerator::mem_write_list_t;
+  /// Type for caching the generated expressions.
+  using ExprMap = VerilogGenerator::ExprMap;
+  // VerilogGen Configure
+  /// the structure to configure the verilog generator
+  using VlgGenConfig = VerilogGenerator::VlgGenConfig;
+  /// Type of function apply record
+  using function_app_t = VerilogGenerator::function_app_t;
+  /// Type of func app vector record
+  using function_app_vec_t = VerilogGenerator::function_app_vec_t;
+
+protected:
+  // --------------------- MEMBERS ---------------------------- //
+  vlg_names_t all_decode_signals;
+
+  // --------------------- HELPER FUNCTIONS ---------------------------- //
+  /// Handle function application , Caller: translateBoolOp, translateBvOp
+  virtual vlg_name_t translateApplyFunc(std::shared_ptr<ExprOpAppFunc> func_app_ptr_) override;
+
+  /// called by ParseNonMemUpdateExpr to deal with a boolop node
+  virtual vlg_name_t translateBoolOp(const std::shared_ptr<ExprOp>& e) override;
+  /// called by ParseNonMemUpdateExpr to deal with a bvop node
+  virtual vlg_name_t translateBvOp(const std::shared_ptr<ExprOp>& e) override;
+  /// travserse an expression, not used as mem-write subtree
+  virtual void ParseNonMemUpdateExpr(const ExprPtr& e);
+
+public:
+  // --------------------- CONSTRUCTOR ---------------------------- //
+  /// \param[in] Configuration
+  /// \param[in] Top module name, if empty, get it from instruction name
+  /// \param[in] clock signal name
+  /// \param[in] reset signal name
+  VerilogDecodeForAQedGenerator(const VlgGenConfig& config = VlgGenConfig(),
+                   const std::string& modName = "",
+                   const std::string& clk = "clk",
+                   const std::string& rst = "rst");
+  /// Parse an ILA, will gen all its instructions, and get the var used
+  void ExportDecode(const InstrLvlAbsCnstPtr& ila_ptr_, 
+    std::set<ExprPtr> & var_use_in_decodes);
+  /// add a signel and assumption of the allowed sequences --- any single one is good
+  void GenSequenceAssumtionsAny();
+  void GenSequenceOneAtATime();
+
+  // for the trans seq in ILA specification, generate the sequence for it
+  // but you probably need to specify a bound
+  void GenValidSequenceAssumption(const InstrLvlAbsCnstPtr& ila_ptr_);
+
+  /// add a signel and assumption of the allowed sequences --- give a bad state and
+  /// try enumerate sequence with out reaching that state
+  // Not implemented yet
+  void GenSequenceAssumtionsNotBadState();
+}; // class VerilogDecodeForAQedGenerator
+
+}; // namespace ilang
+
+#endif // ILANG_AQED_OUT_VLOG_OUT_H__

include/ilang/verilog-out/verilog_gen.h

@@ -287,8 +287,6 @@ class VerilogGeneratorBase {
   // --------------------- HELPER FUNCTIONS ---------------------------- //
   /// Check if a name is reserved (clk/rst/modulename/decodeName/ctrName)
   bool check_reserved_name(const vlg_name_t& n) const;
-  /// Get the width of an ExprPtr, must be supported sort
-  int static get_width(const ExprPtr& n);
   /// convert a widith to a verilog string
   std::string static WidthToRange(int w);
   /// get a new id
@@ -297,7 +295,9 @@ class VerilogGeneratorBase {
   /// that to the name;
   vlg_name_t new_id(const ExprPtr& e);
 
-public:
+public:  
+  /// Get the width of an ExprPtr, must be supported sort
+  int static get_width(const ExprPtr& n);
   /// sanitize a name string, so it will generate illegal verilog identifier
   static vlg_name_t sanitizeName(const vlg_name_t& n);
   /// sanitize the name of an expr, so it will generate illegal verilog
@@ -424,49 +424,49 @@ class VerilogGenerator : public VerilogGeneratorBase {
   /// Type of func app vector record
   using function_app_vec_t = VerilogGeneratorBase::function_app_vec_t;
 
-private:
+protected:
   // --------------------- HELPER FUNCTIONS ---------------------------- //
   /// handle a input variable (memvar/bool/bv)
-  void insertInput(const ExprPtr& input);
+  virtual void insertInput(const ExprPtr& input);
   /// handle a state variable
-  void insertState(const ExprPtr& state);
+  virtual void insertState(const ExprPtr& state);
 
   // Here we are not using depthfirstSearch as we need to alternate between
   // root-first/root-last traversal
   /// traverse to the subtree, caller: ParseNonMemUpdateExpr
-  void parseArg(const ExprPtr& e);
+  virtual void parseArg(const ExprPtr& e);
   /// After you parse a subtree, this can help you get the vlg name associated
   /// with it
-  VerilogGenerator::vlg_name_t getVlgFromExpr(const ExprPtr& e);
+  virtual VerilogGenerator::vlg_name_t getVlgFromExpr(const ExprPtr& e);
   /// a short cut of calling getVlgFromExpr to find arg's vlg names
-  VerilogGenerator::vlg_name_t getArg(const ExprPtr& e, const size_t& i);
+  virtual VerilogGenerator::vlg_name_t getArg(const ExprPtr& e, const size_t& i);
   /// Handle function application , Caller: translateBoolOp, translateBvOp
-  vlg_name_t translateApplyFunc(std::shared_ptr<ExprOpAppFunc> func_app_ptr_);
+  virtual vlg_name_t translateApplyFunc(std::shared_ptr<ExprOpAppFunc> func_app_ptr_);
   /// called by ParseNonMemUpdateExpr to deal with a boolop node
-  vlg_name_t translateBoolOp(const std::shared_ptr<ExprOp>& e);
+  virtual vlg_name_t translateBoolOp(const std::shared_ptr<ExprOp>& e);
   /// called by ParseNonMemUpdateExpr to deal with a bvop node
-  vlg_name_t translateBvOp(const std::shared_ptr<ExprOp>& e);
+  virtual vlg_name_t translateBvOp(const std::shared_ptr<ExprOp>& e);
   /// travserse an expression, not used as mem-write subtree
-  void ParseNonMemUpdateExpr(const ExprPtr& e);
+  virtual void ParseNonMemUpdateExpr(const ExprPtr& e);
   /// check if a mem-write subtree is what we can handle right now
-  bool CheckMemUpdateNode(const ExprPtr& e, const std::string& mem_var_name);
+  virtual bool CheckMemUpdateNode(const ExprPtr& e, const std::string& mem_var_name);
   /// traverse the memory-write subtree of "e", its upper level has the
   /// condition "cond"
-  void VisitMemNodes(const ExprPtr& e, const ExprPtr& cond,
+  virtual void VisitMemNodes(const ExprPtr& e, const ExprPtr& cond,
                      mem_write_entry_list_stack_t& writesStack);
 
   /// add signals & stmts for an internal counter to trace start (more not be
   /// useful)
   void addInternalCounter(vlg_name_t decode_sig_name, size_t width = 8);
   /// use: func_ptr_set ;  affect: prehear, only export if func is internal
-  void ExportFuncDefs();
+  virtual void ExportFuncDefs();
 
   /// generate the signals to write a memory (external/internal)
-  void ExportCondWrites(const ExprPtr& mem_var,
+  virtual void ExportCondWrites(const ExprPtr& mem_var,
                         const mem_write_list_t& writeList);
   /// parse an expr used as the memory update, will affect: past_writes &
   /// current_writes
-  void ParseMemUpdateNode(const ExprPtr& cond, const ExprPtr& e,
+  virtual void ParseMemUpdateNode(const ExprPtr& cond, const ExprPtr& e,
                           const std::string& mem_var_name);
 
 public:
@@ -480,9 +480,9 @@ class VerilogGenerator : public VerilogGeneratorBase {
                    const std::string& clk = "clk",
                    const std::string& rst = "rst");
   /// Parse an ILA, will gen all its instructions
-  void ExportIla(const InstrLvlAbsPtr& ila_ptr_);
+  void ExportIla(const InstrLvlAbsCnstPtr & ila_ptr_);
   /// Parse an instruction
-  void ExportTopLevelInstr(const InstrPtr& instr_ptr_);
+  void ExportTopLevelInstr(const InstrCnstPtr & instr_ptr_);
 }; // class VerilogGenerator
 
 }; // namespace ilang

include/ilang/vtarget-out/directive.h

@@ -69,6 +69,8 @@ class IntefaceDirectiveRecorder {
   static bool beginsWith(const std::string& c, const std::string& s);
   /// Return true if 'c' is special input directive
   static bool isSpecialInputDir(const std::string& c);
+  // Return nonempty string if 'c' has special reset signal in its encoding
+  static std::string isSpecialInputDirResetName(const std::string& c);
   /// Check for compatibility
   static bool isSpecialInputDirCompatibleWith(const std::string& c,
                                               const SignalInfoBase& vlg_sig);