{"id":"W1574510674","doi":"10.1109/iscas.1999.777794","title":"Synthesis of checker EFSMs from timing diagram specifications","year":2003,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université de Montréal","funders":"","keywords":"Computer science; Verilog; VHDL; Emulation; Formal verification; Embedded system; Model checking; PCI configuration space; Formal equivalence checking; Hardware description language; Protocol (science); Hardware emulation; Computer architecture; Programming language; Field-programmable gate array; PCI Express","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.001643153,0.0008091434,0.0004745913,0.001182715,0.0002790223,0.0008873165,0.0006691059,0.0006435688,0.004705996],"category_scores_gemma":[0.007283724,0.0005256377,0.0008210079,0.0005371929,0.0005714328,0.0008572261,0.0005988443,0.0007894156,0.001012773],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0005837362,"about_ca_system_score_gemma":0.001459267,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00147183,"about_ca_topic_score_gemma":0.002515162,"domain_scores_codex":[0.9987717,0.000360382,0.0001435841,0.0001542994,0.0004266778,0.0001433124],"domain_scores_gemma":[0.9951158,0.003155939,0.0004362743,0.0006371051,0.00059197,0.0000629561],"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.0005139395,0.0002636687,0.002844355,0.001250853,0.0001412871,0.000999096,0.0004998397,0.3700802,0.08918896,0.1776458,0.005903932,0.350668],"study_design_scores_gemma":[0.0002560841,0.0002551918,0.0005827967,0.000160754,0.000108375,0.0002423943,0.00008915045,0.7911027,0.1331217,0.05484395,0.01920012,0.00003659561],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02809943,0.0001277337,0.9605041,0.0001011968,0.00006145384,0.0001911987,0.0004567036,0.00613892,0.004319163],"genre_scores_gemma":[0.3415426,0.000224083,0.6524746,0.0001405349,0.00003502213,0.0003926614,0.00142887,0.0005544598,0.003207119],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.004705996,"threshold_uncertainty_score":0.01574314,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1024225399458173,"score_gpt":0.2988785508138963,"score_spread":0.196456010868079,"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."}}