ilang  0.9.1
ILAng: A Modeling and Verification Platform for SoCs
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
ilang::VlgSglTgtGen_Jasper Class Reference

Verilog Verification Target Generator – for JasperGold Unlike for cosa, we don't need a separate file although we do have some ... More...

#include <vtarget_gen_jasper.h>

Inheritance diagram for ilang::VlgSglTgtGen_Jasper:
ilang::VlgSglTgtGen

Public Member Functions

 VlgSglTgtGen_Jasper (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, 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 > &include_dirs, const vtg_config_t &vtg_config, backend_selector backend)
 
void add_addition_clock_info (const std::string &expr)
 
void add_addition_reset_info (const std::string &expr)
 
virtual void do_not_instantiate (void) override
 It is okay to instantiation.
 
- Public Member Functions inherited from 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, 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)
 
virtual ~VlgSglTgtGen ()
 Destructor: do nothing , most importantly it is virtual.
 
virtual void ConstructWrapper ()
 
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 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.
 
bool in_bad_state (void) const
 check if this module is in a bad state
 

Protected Member Functions

virtual void add_an_assumption (const std::string &aspt, const std::string &dspt) override
 Add an assumption.
 
virtual void add_an_assertion (const std::string &asst, const std::string &dspt) override
 Add an assertion.
 
virtual void add_a_direct_assumption (const std::string &aspt, const std::string &dspt) override
 Add a direct assumption.
 
virtual void add_a_direct_assertion (const std::string &asst, const std::string &dspt) override
 Add a direct assertion.
 
virtual void add_wire_assign_assumption (const std::string &varname, const std::string &expression, const std::string &dspt) override
 
virtual void add_reg_cassign_assumption (const std::string &varname, const std::string &expression, const std::string &cond, const std::string &dspt) override
 
virtual void Export_script (const std::string &script_name) override
 export the script to run the verification
 
virtual void Export_problem (const std::string &extra_name) override
 export extra things (problem)
 
virtual void Export_mem (const std::string &mem_name) override
 
virtual void Export_modify_verilog () override
 For jasper, this means do nothing, for yosys, you need to add (keep)
 
- Protected Member Functions inherited from ilang::VlgSglTgtGen
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_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_assumptions ()
 Add invariants as assumptions.
 
void ConstructWrapper_add_inv_assertions ()
 Add invariants as assertions.
 
void ConstructWrapper_add_additional_mapping_control ()
 Add more assumptions/assertions.
 
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.
 
std::string ConstructWrapper_get_ila_module_inst ()
 get the ila module instantiation string
 
bool bad_state_return (void)
 If it is bad state, return true and display a message.
 

Protected Attributes

std::vector< std::pair< std::string, std::string > > assumptions
 
std::vector< std::pair< std::string, std::string > > assertions
 vector of pairs of <assertions, description>
 
std::vector< std::string > additional_clock_expr
 vector of clock signals that need to be taken care of
 
std::vector< std::string > additional_reset_expr
 vector of clock signals that need to be taken care of
 
std::string jg_script_name
 Name of the problem file.
 
std::string abs_mem_name
 Name of the problem file.
 
- Protected Attributes inherited from ilang::VlgSglTgtGen
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
 
VerilogInfovlg_info_ptr
 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.
 
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
 
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.
 
backend_selector _backend
 Store the selection of backend.
 

Additional Inherited Members

- Public Types inherited from ilang::VlgSglTgtGen
enum  target_type_t { INVARIANTS, INSTRUCTIONS }
 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 backend.
 
using vtg_config_t = VlgVerifTgtGenBase::vtg_config_t
 Type of configuration.
 
- Static Protected Member Functions inherited from ilang::VlgSglTgtGen
static unsigned TypeMatched (const ExprPtr &ila_var, const SignalInfoBase &vlg_var)
 
static unsigned get_width (const ExprPtr &n)
 get width of an ila node
 

Detailed Description

Verilog Verification Target Generator – for JasperGold Unlike for cosa, we don't need a separate file although we do have some ...

Constructor & Destructor Documentation

◆ VlgSglTgtGen_Jasper()

ilang::VlgSglTgtGen_Jasper::VlgSglTgtGen_Jasper ( 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,
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 > &  include_dirs,
const vtg_config_t vtg_config,
backend_selector  backend 
)
Parameters
[in]outputpath (ila-verilog, wrapper-verilog, problem.txt, run-verify-by-???, modify-impl, it there is )
[in]pointerto the instruction
[in]thedefault configuration for outputing verilog
[in]thevariable map
[in]theconditions
[in]pointerto verify info class
[in]verilogmodule name
[in]ilamodule name,
[in]allimplementation sources
[in]allinclude paths
[in]whichbackend to use, it needs this info to gen proper properties

Member Function Documentation

◆ add_addition_clock_info()

void ilang::VlgSglTgtGen_Jasper::add_addition_clock_info ( const std::string &  expr)

if you have signals that are controled by assumptions to be equal as the outer clock, you need to put them here, because the assumptions do not work in the jaspergold reset step (unlike COSA)

◆ add_reg_cassign_assumption()

virtual void ilang::VlgSglTgtGen_Jasper::add_reg_cassign_assumption ( const std::string &  varname,
const std::string &  expression,
const std::string &  cond,
const std::string &  dspt 
)
overrideprotectedvirtual

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

Implements ilang::VlgSglTgtGen.

◆ add_wire_assign_assumption()

virtual void ilang::VlgSglTgtGen_Jasper::add_wire_assign_assumption ( const std::string &  varname,
const std::string &  expression,
const std::string &  dspt 
)
overrideprotectedvirtual

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

Implements ilang::VlgSglTgtGen.

◆ Export_mem()

virtual void ilang::VlgSglTgtGen_Jasper::Export_mem ( const std::string &  mem_name)
overrideprotectedvirtual

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

Implements ilang::VlgSglTgtGen.

Member Data Documentation

◆ assumptions

std::vector<std::pair<std::string, std::string> > ilang::VlgSglTgtGen_Jasper::assumptions
protected

internal storage of problems vector of pairs of <assumption, description>


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