{"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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0003842788,0.0000700817,0.0001071755,0.0000605224,0.00005072734,0.00003629684,0.0004901836,0.0000430999,0.0001760882],"category_scores_gemma":[0.0005575203,0.00006290751,0.00004460461,0.000314039,0.00004102343,0.0002912967,0.0000400254,0.00005267465,0.0001188737],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002252644,"about_ca_system_score_gemma":0.00002681164,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00003707546,"about_ca_topic_score_gemma":0.000002051706,"domain_scores_codex":[0.9991603,0.0001119568,0.000226942,0.0002185136,0.0001606321,0.0001215866],"domain_scores_gemma":[0.9988672,0.0001935236,0.00009609367,0.0007376912,0.00006154452,0.0000440016],"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":[7.271364e-7,0.00005867468,0.0006208448,0.000003376416,0.000009693289,2.734912e-7,0.00025132,0.00002404335,0.005428668,0.9366941,0.0002375146,0.05667079],"study_design_scores_gemma":[0.00007232239,0.00001380784,0.01894526,0.00001380687,0.000009491393,0.000001938391,0.00007664159,0.0330412,0.9300719,0.01013112,0.007458275,0.000164265],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.008147912,0.00003465821,0.9356046,0.00008560337,0.0001974759,0.00007770433,0.000002047442,0.00008243634,0.05576755],"genre_scores_gemma":[0.3436786,0.000009297489,0.6560823,0.00002700083,0.00001091117,0.00001544737,5.669706e-7,0.000003487307,0.0001723795],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.926563,"threshold_uncertainty_score":0.2565294,"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."}}