ilang  1.0.2
ILAng: A Modeling and Verification Platform for SoCs
Public Types | Public Member Functions | Protected Member Functions | Static Protected Member Functions | Protected Attributes | List of all members
ilang::VlgSglTgtGen Class Referenceabstract

Generating a target (just the invairant or for an instruction) More...

#include <vtarget_gen_impl.h>

Inheritance diagram for ilang::VlgSglTgtGen:
ilang::VlgSglTgtGen_Cosa ilang::VlgSglTgtGen_Jasper ilang::VlgSglTgtGen_Yosys

Public Types

 Type of the target.
enum  ready_type_t { NA = 0, READY_SIGNAL = 1, READY_BOUND = 2, BOTH = 3 }
 Type of the ready condition.
typedef std::map< std::string, unsigned > func_app_cnt_t
 Per func apply counter.
using backend_selector = VlgVerifTgtGenBase::backend_selector
 Type of the verification backend.
using synthesis_backend_selector = VlgVerifTgtGenBase::synthesis_backend_selector
 Type of the synthesis backend.
using vtg_config_t = VlgVerifTgtGenBase::vtg_config_t
 Type of configuration.
using ex_info_t = VlgVerifTgtGenBase::ex_info_t
 Type of record of extra info of a signal.
using advanced_parameters_t = VlgVerifTgtGenBase::advanced_parameters_t
 Type of advanced parameter.

Public Member Functions

 VlgSglTgtGen (const std::string &output_path, const InstrPtr &instr_ptr, const InstrLvlAbsPtr &ila_ptr, const VerilogGenerator::VlgGenConfig &config, nlohmann::json &_rf_vmap, nlohmann::json &_rf_cond, VlgTgtSupplementaryInfo &_supplementary_info, VerilogInfo *_vlg_info_ptr, const std::string &vlg_mod_inst_name, const std::string &ila_mod_inst_name, const std::string &wrapper_name, const std::vector< std::string > &implementation_srcs, const std::vector< std::string > &implementation_include_path, const vtg_config_t &vtg_config, backend_selector backend, const target_type_t &target_tp, advanced_parameters_t *adv_ptr)
virtual ~VlgSglTgtGen ()
 Destructor: do nothing , most importantly it is virtual.
virtual void ConstructWrapper ()
virtual void PreExportProcess ()=0
 PreExportWork (modification and etc.)
virtual void Export_wrapper (const std::string &wrapper_name)
 create the wrapper file
virtual void Export_ila_vlg (const std::string &ila_vlg_name)
 export the ila verilog
virtual void Export_script (const std::string &script_name)=0
 export the script to run the verification
virtual void Export_problem (const std::string &extra_name)=0
 export extra things (problem)
virtual void Export_mem (const std::string &mem_name)=0
virtual void Export_modify_verilog ()=0
 For jasper, this means do nothing, for yosys, you need to add (keep)
virtual void ExportAll (const std::string &wrapper_name, const std::string &ila_vlg_name, const std::string &script_name, const std::string &extra_name, const std::string &mem_name)
 Take care of exporting all of a single target.
virtual void do_not_instantiate (void)=0
bool in_bad_state (void) const
 check if this module is in a bad state

Protected Member Functions

std::string new_mapping_id ()
 Return a new variable name for mapping.
std::string new_property_id ()
 Return a new variable name for property.
const ExprPtr IlaGetState (const std::string &sname) const
 Get the pointer of a ila state, it must exist.
const ExprPtr IlaGetInput (const std::string &sname) const
 Get the pointer of an ila input, it must exist.
std::pair< unsigned, unsigned > GetMemInfo (const std::string &ila_mem_name) const
 Get (a,d) width of a memory, if not existing, (0,0)
bool TryFindIlaState (const std::string &sname)
 Test if a string represents an ila state name.
bool TryFindIlaInput (const std::string &sname)
 Test if a string represents an ila input name.
bool TryFindVlgState (const std::string &sname)
 Test if a string represents a Verilog signal name.
ExprPtr TryFindIlaVarName (const std::string &sname)
 Try to find a ILA var according to a name.
std::string ModifyCondExprAndRecordVlgName (const VarExtractor::token &t)
 Modify a token and record its use.
std::string ReplExpr (const std::string &expr, bool force_vlg_sts=false)
 Parse and modify a condition string.
std::string PerStateMap (const std::string &ila_state_name_or_equ, const std::string &vlg_st_name)
 handle a single string map (s-name/equ-string)
std::string GetStateVarMapExpr (const std::string &ila_state_name, nlohmann::json &m, bool is_assert=false)
void handle_start_condition (nlohmann::json &dc)
 add a start condition if it is given
nlohmann::json & get_current_instruction_rf ()
 Find the current instruction mapping.
void ConstructWrapper_add_ila_input ()
 add ila input to the wrapper
void ConstructWrapper_reset_setup ()
 setup reset, add assumptions if necessary
void ConstructWrapper_add_vlg_input_output ()
 add the vlg input ouput to the wrapper I/O
void ConstructWrapper_add_cycle_count_moniter ()
 add a cycle counter to be used to deal with the end cycle
void ConstructWrapper_generate_header ()
 generate the `define TRUE 1
void ConstructWrapper_add_varmap_assumptions ()
 add state equ assumptions
void ConstructWrapper_add_varmap_assertions ()
 add state equ assertions
void ConstructWrapper_add_inv_assumption_or_assertion_target_invariant ()
 Add invariants as assumption/assertion when target is invariant.
void ConstructWrapper_add_inv_assumption_or_assertion_target_instruction ()
 Add invariants as assumption/assertion when target is instruction.
void ConstructWrapper_add_additional_mapping_control ()
 Add more assumptions for mapping (only use for instruction target)
void ConstructWrapper_add_rf_assumptions ()
 Add more assumptions for I/O for example (both instruction/invariant)
void ConstructWrapper_add_condition_signals ()
 Generate ISSUE, IEND, ... signals.
void ConstructWrapper_register_extra_io_wire ()
 Register the extra wires to the idr.
void ConstructWrapper_add_module_instantiation ()
 Add instantiation statement of the two modules.
void ConstructWrapper_add_helper_memory ()
void ConstructWrapper_add_uf_constraints ()
 Add buffers and assumption/assertions about the.
void ConstructWrapper_add_post_value_holder ()
 Add post value holder (val @ cond == ...)
int ConstructWrapper_add_post_value_holder_handle_obj (nlohmann::json &pv_cond_val, const std::string &pv_name, int width, bool create_reg)
 A sub function of the above post-value-holder hanlder.
void ConstructWrapper_add_vlg_monitor ()
 Add Verilog inline monitor.
void ConstructWrapper_add_inv_assumption_or_assertion_target_inv_syn_design_only ()
 Add invariants as assumption/assertion when target is inv_syn_design_only.
void ConstructWrapper_inv_syn_connect_mem ()
 Connect the memory even we don't care a lot about them.
void ConstructWrapper_inv_syn_cond_signals ()
std::string ConstructWrapper_get_ila_module_inst ()
 get the ila module instantiation string
void add_inv_obj_as_assertion (InvariantObject *inv_obj)
 add an invariant object as assertion
void add_inv_obj_as_assumption (InvariantObject *inv_obj)
 add an invariant object as an assumption
void add_rf_inv_as_assumption ()
 add rf inv as assumptions (if there are)
void add_rf_inv_as_assertion ()
 add rf inv as assumptions (if there are)
virtual void add_a_direct_assumption (const std::string &aspt, const std::string &dspt)=0
 Add an assumption – backend dependent.
virtual void add_a_direct_assertion (const std::string &asst, const std::string &dspt)=0
 Add an assertion.
virtual void add_an_assumption (const std::string &aspt, const std::string &dspt)
 Add an assumption – JasperGold will override this.
virtual void add_an_assertion (const std::string &asst, const std::string &dspt)
 Add an assertion – JasperGold will override this.
virtual void add_wire_assign_assumption (const std::string &varname, const std::string &expression, const std::string &dspt)
virtual void add_reg_cassign_assumption (const std::string &varname, const std::string &expression, int width, const std::string &cond, const std::string &dspt)
bool bad_state_return (void)
 If it is bad state, return true and display a message.

Static Protected Member Functions

static unsigned TypeMatched (const ExprPtr &ila_var, const SignalInfoBase &vlg_var)
static unsigned get_width (const ExprPtr &n)
 get width of an ila node

Protected Attributes

const std::string _output_path
InstrPtr _instr_ptr
 The pointer to the instruction that is going to export.
InstrLvlAbsPtr _host
 The pointer to the host ila.
const std::string _vlg_mod_inst_name
 The name of verilog top module instance in the wrapper.
const std::string _ila_mod_inst_name
 The name of ila-verilog top module instance in the wrapper.
VerilogGeneratorBase vlg_wrapper
 Generator for the wrapper module.
VerilogGenerator vlg_ila
 Generator for the ila verilog.
IntefaceDirectiveRecorder _idr
 inteface directive recorder
StateMappingDirectiveRecorder _sdr
 state directive recorder
 Analyzer for the implementation.
VarExtractor _vext
 variable extractor to handle property expressions
nlohmann::json & rf_vmap
 refinement relation variable mapping
nlohmann::json & rf_cond
 refinement relation instruction conditions
nlohmann::json empty_json
 An empty json for default fallthrough cases.
const VlgTgtSupplementaryInfosupplementary_info
 The supplementary information.
std::map< std::string, ex_info_t_all_referred_vlg_names
 record all the referred vlg names, so you can add (keep) if needed
target_type_t target_type
 target type
bool has_flush
 a shortcut of whether rf has flush condition set
ready_type_t ready_type
 ready type
func_app_cnt_t func_cnt
 func apply counter
unsigned max_bound
 max bound , default 127
unsigned cnt_width
 the width of the counter
 to store the advanced parameter configurations
const bool has_gussed_synthesized_invariant
 has guessed synthesized invariant
const bool has_confirmed_synthesized_invariant
 has confirmed synthesized invariant
const bool has_rf_invariant
 has rf provided invariant
std::string top_mod_name
 top verilog module name
std::string top_file_name
 top verilog module file
std::string ila_file_name
 top verilog module file
std::vector< std::string > vlg_design_files
 design files
std::vector< std::string > vlg_include_files_path
 include paths
vtg_config_t _vtg_config
 Store the configuration.
const VerilogGenerator::VlgGenConfig_vlg_cfg
 Store the vlg configurations.
backend_selector _backend
 Store the selection of backend.

Detailed Description

Generating a target (just the invairant or for an instruction)

Constructor & Destructor Documentation

◆ VlgSglTgtGen()

ilang::VlgSglTgtGen::VlgSglTgtGen ( const std::string &  output_path,
const InstrPtr instr_ptr,
const InstrLvlAbsPtr ila_ptr,
const VerilogGenerator::VlgGenConfig config,
nlohmann::json &  _rf_vmap,
nlohmann::json &  _rf_cond,
VlgTgtSupplementaryInfo _supplementary_info,
VerilogInfo _vlg_info_ptr,
const std::string &  vlg_mod_inst_name,
const std::string &  ila_mod_inst_name,
const std::string &  wrapper_name,
const std::vector< std::string > &  implementation_srcs,
const std::vector< std::string > &  implementation_include_path,
const vtg_config_t vtg_config,
backend_selector  backend,
const target_type_t target_tp,
advanced_parameters_t adv_ptr 
[in]outputpath (ila-verilog, wrapper-verilog, problem.txt, run-verify-by-???, modify-impl, it there is )
[in]pointerto the instruction
[in]thehost ila
[in]thedefault configuration for outputing verilog
[in]thevariable map
[in]pointerto verify info class
[in]verilogmodule name
[in]ilamodule name
[in]verilogwrapper module name
[in]implemenationsources, can be used to modify and copy
[in]allinclude paths
[in]whichbackend to use, it needs this info to gen proper properties

Member Function Documentation

◆ add_reg_cassign_assumption()

virtual void ilang::VlgSglTgtGen::add_reg_cassign_assumption ( const std::string &  varname,
const std::string &  expression,
int  width,
const std::string &  cond,
const std::string &  dspt 

Add an assignment to a register which in JasperGold could be an assignment, but in CoSA has to be an assumption

Reimplemented in ilang::VlgSglTgtGen_Jasper.

◆ add_wire_assign_assumption()

virtual void ilang::VlgSglTgtGen::add_wire_assign_assumption ( const std::string &  varname,
const std::string &  expression,
const std::string &  dspt 

Add an assignment which in JasperGold could be an assignment, but in CoSA has to be an assumption

Reimplemented in ilang::VlgSglTgtGen_Jasper.

◆ ConstructWrapper()

virtual void ilang::VlgSglTgtGen::ConstructWrapper ( )

Call the separate construct functions to make a wrapper (not yet export it)

◆ ConstructWrapper_add_helper_memory()

void ilang::VlgSglTgtGen::ConstructWrapper_add_helper_memory ( )

Add instantiation of the memory and put the needed mem implementation in extra export This also include the assertions

◆ ConstructWrapper_inv_syn_cond_signals()

void ilang::VlgSglTgtGen::ConstructWrapper_inv_syn_cond_signals ( )

Sometimes you need to add some signals that only appeared in Instruction target

◆ Export_mem()

virtual void ilang::VlgSglTgtGen::Export_mem ( const std::string &  mem_name)
pure virtual

export the memory abstraction (implementation) Yes, this is also implementation specific, (jasper may use a different one)

Implemented in ilang::VlgSglTgtGen_Yosys, ilang::VlgSglTgtGen_Cosa, and ilang::VlgSglTgtGen_Jasper.

◆ GetStateVarMapExpr()

std::string ilang::VlgSglTgtGen::GetStateVarMapExpr ( const std::string &  ila_state_name,
nlohmann::json &  m,
bool  is_assert = false 

handle a var map will create new variables "m?" and return it

  1. "ila-state":"**MEM**.?" 2a. "ila-state":"statename" --> PerStateMap 2b. "ila-state":"(cond)&map" --> PerStateMap
  2. "ila-state":[ "cond&map" ]
  3. "ila-state":[ {"cond":,"map":}, ]

◆ TypeMatched()

static unsigned ilang::VlgSglTgtGen::TypeMatched ( const ExprPtr ila_var,
const SignalInfoBase vlg_var 

Check if ila name and vlg name are type compatible (not including special directives)

Member Data Documentation

◆ _output_path

const std::string ilang::VlgSglTgtGen::_output_path

output path, output the ila-verilog, wrapper-verilog, problem.txt, run-verify-by-???

The documentation for this class was generated from the following file: