{"id":"W2078940150","doi":"10.1109/tcad.2013.2278491","title":"Debugging RTL Using Structural Dominance","year":2014,"lang":"en","type":"article","venue":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":10,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Computer science; Debugging; Bottleneck; Boolean satisfiability problem; Speedup; Parallel computing; Formal equivalence checking; Theoretical computer science; Programming language; Formal verification; Algorithm; Embedded system","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001727759,0.001366088,0.0007072028,0.002052624,0.0007872405,0.001257036,0.001308106,0.0007463604,0.004578695],"category_scores_gemma":[0.009110223,0.000801498,0.001129831,0.0007537309,0.001018606,0.002232458,0.002068713,0.001062365,0.0009320421],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001039005,"about_ca_system_score_gemma":0.002457242,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004354976,"about_ca_topic_score_gemma":0.008788154,"domain_scores_codex":[0.9976571,0.0007975887,0.0001059537,0.0003836099,0.0008278295,0.0002279308],"domain_scores_gemma":[0.9948105,0.003398519,0.0004699297,0.000543932,0.0006803386,0.00009679142],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0003479377,0.000173644,0.004696933,0.0004228604,0.00009525513,0.0005707182,0.0006056179,0.4602651,0.06804397,0.07031471,0.003776535,0.3906867],"study_design_scores_gemma":[0.00004622289,0.0001271019,0.000345628,0.00004668611,0.00003301445,0.0001982162,0.00006327658,0.9359437,0.02355368,0.03561612,0.003995275,0.00003107377],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02862164,0.0001718506,0.9645814,0.000159177,0.00002288725,0.00008096432,0.0001175651,0.00289621,0.003348431],"genre_scores_gemma":[0.4547459,0.0002763155,0.5402189,0.0001916895,0.0000363163,0.0001776533,0.0004901385,0.0006838332,0.003179169],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.004578695,"threshold_uncertainty_score":0.01531732,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05249852120037057,"score_gpt":0.2731716530537248,"score_spread":0.2206731318533542,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}