{"id":"W1568724472","doi":"","title":"A formal verification framework for Bluespec System Verilog","year":2013,"lang":"en","type":"article","venue":"HAL (Le Centre pour la Communication Scientifique Directe)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":13,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Systems Modeling Language; Computer science; Correctness; Activity diagram; Programming language; Formal equivalence checking; Formal verification; Verilog; Unified Modeling Language; Hardware description language; Probabilistic logic; Formal methods; Theoretical computer science; Embedded system; Field-programmable gate array; Software; Artificial intelligence","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.002763486,0.0009878088,0.0006610035,0.001139821,0.0006472792,0.002173248,0.001747817,0.0009096017,0.01004428],"category_scores_gemma":[0.004501755,0.001105645,0.00138857,0.00048033,0.00150604,0.002498208,0.001788529,0.002273275,0.00274168],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0009699932,"about_ca_system_score_gemma":0.002709003,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004007003,"about_ca_topic_score_gemma":0.004918642,"domain_scores_codex":[0.9983891,0.0004644262,0.0001235336,0.0002381754,0.0005855911,0.0001992311],"domain_scores_gemma":[0.9971945,0.001639009,0.0001648234,0.0004944394,0.0004321992,0.00007493147],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0003939081,0.0002824356,0.001137839,0.001484892,0.0001214005,0.0009461191,0.0006996465,0.1280019,0.03528322,0.4851902,0.02256438,0.3238941],"study_design_scores_gemma":[0.0002505405,0.000258451,0.0004956402,0.0005294686,0.0001615819,0.0007843889,0.0001304012,0.5158536,0.0489478,0.2929917,0.1394613,0.0001350998],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.001583335,0.0001049813,0.987328,0.0001144532,0.00004468113,0.00009417482,0.0001731628,0.008693413,0.001863916],"genre_scores_gemma":[0.170172,0.0005465416,0.815046,0.0005472008,0.0001278793,0.0003926899,0.001038407,0.003584043,0.00854533],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01004428,"threshold_uncertainty_score":0.03360146,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01789563312264643,"score_gpt":0.2477536717900701,"score_spread":0.2298580386674237,"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."}}