{"id":"W2134227513","doi":"10.1109/ccece.2007.355","title":"Formal Verification of System Level Designs: A GSM Vocoder Case Study","year":2007,"lang":"en","type":"article","venue":"","topic":"Embedded Systems Design Techniques","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; SystemC; GSM; Abstraction; Concurrency; Electronic system-level design and verification; Formal verification; Set (abstract data type); Encoder; Formal methods; Formal specification; Embedded system; Programming language; Computer network","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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002858948,0.0001368891,0.0002172697,0.0002155602,0.00009111549,0.00005689847,0.0006231706,0.00007874491,0.00000233227],"category_scores_gemma":[0.00001815328,0.000116947,0.00005204188,0.0004250474,0.00002194538,0.0007250637,0.0001316398,0.00008169071,0.00001737965],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001103184,"about_ca_system_score_gemma":0.00005707174,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0008603501,"about_ca_topic_score_gemma":0.0001474098,"domain_scores_codex":[0.9982834,0.0001420647,0.0006065314,0.0003191521,0.0003601069,0.0002887708],"domain_scores_gemma":[0.998452,0.0001237472,0.0002129537,0.0009053038,0.0002290676,0.00007690469],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.00009544205,0.002360476,0.01054272,0.001105236,0.0002797215,0.009566897,0.04942623,0.00006159345,0.100702,0.7101645,0.002535154,0.11316],"study_design_scores_gemma":[0.00322761,0.00355024,0.007223716,0.0004504506,0.00009041145,0.02249871,0.06482285,0.1104045,0.7847291,0.0009086654,0.0003641938,0.001729669],"study_design_candidate":"bench_or_experimental","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.1093718,0.00002240237,0.8851482,0.000005986156,0.0001110276,0.0009398367,8.789747e-7,0.0005510876,0.003848755],"genre_scores_gemma":[0.8444811,1.945082e-7,0.1552484,0.00001513471,0.00002451525,0.00004375464,3.243693e-7,0.000008912387,0.0001776751],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.7351093,"threshold_uncertainty_score":0.476896,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1197747995771805,"score_gpt":0.3304533327827936,"score_spread":0.2106785332056131,"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."}}