From 2da94bda1ebc0ccd881093279b0977b58d40db3e Mon Sep 17 00:00:00 2001 From: DanieCuevas <43822444+DanielCuevas1208@users.noreply.github.com> Date: Tue, 4 Aug 2026 03:01:30 -0700 Subject: [PATCH 1/2] feat: extend gatework --- .github/workflows/ci.yml | 4 ++ .gitignore | 2 + CHANGELOG.md | 14 ++++++ README.md | 80 ++++++++++++++++++++++++++++++++--- fixtures/adder.golden.vcd | 2 +- fixtures/assert.golden.vcd | 2 +- fixtures/asymdelay.golden.vcd | 2 +- fixtures/buffer.golden.vcd | 41 ++++++++++++++++++ fixtures/buffer.net | 17 ++++++++ fixtures/bus.golden.vcd | 2 +- fixtures/counter.golden.vcd | 2 +- fixtures/delay.golden.vcd | 2 +- fixtures/gates.golden.vcd | 2 +- fixtures/haddader.golden.vcd | 2 +- fixtures/hcounter.golden.vcd | 2 +- fixtures/libadder.golden.vcd | 2 +- fixtures/reg2.golden.vcd | 2 +- fixtures/register.golden.vcd | 2 +- fixtures/reset.golden.vcd | 2 +- fixtures/shared.golden.vcd | 2 +- fixtures/tco.golden.vcd | 2 +- fixtures/tristate.golden.vcd | 2 +- fixtures/unknown.golden.vcd | 2 +- fixtures/vector4.golden.vcd | 2 +- gatework.cabal | 3 +- src/Gatework/Logic.hs | 11 ++++- test/Spec.hs | 73 ++++++++++++++++++++++++++++++++ 27 files changed, 256 insertions(+), 25 deletions(-) create mode 100644 fixtures/buffer.golden.vcd create mode 100644 fixtures/buffer.net diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 841c281..bae1771 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -108,6 +108,10 @@ jobs: run: cabal run gatework -- --netlist fixtures/tco.net --duration 22 --output /tmp/tco.vcd --set d=1 --at 4 d=0 --at 8 d=1 --at 14 rst=1 --at 16 rst=0 - name: Compare the clock-to-output delay demo with the golden file run: diff fixtures/tco.golden.vcd /tmp/tco.vcd + - name: Run the buffer demo + run: cabal run gatework -- --netlist fixtures/buffer.net --duration 8 --output /tmp/buffer.vcd --set d=0 --at 2 d=1 --at 4 d=0 --at 6 d=z + - name: Compare the buffer demo with the golden file + run: diff fixtures/buffer.golden.vcd /tmp/buffer.vcd - name: Confirm a missing library file stops the run run: | if cabal run gatework -- --netlist fixtures/libadder.net --library fixtures/missing.net --duration 0 --output /tmp/none.vcd 2>/tmp/none.log; then diff --git a/.gitignore b/.gitignore index 2fae983..9d01073 100644 --- a/.gitignore +++ b/.gitignore @@ -5,6 +5,8 @@ dist-newstyle/ *.dyn_o *.vcd !fixtures/*.golden.vcd +*.report +!fixtures/*.golden.report .haskell-tools/ .stack-work/ .idea/ diff --git a/CHANGELOG.md b/CHANGELOG.md index 8f43dea..649627f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,20 @@ All notable changes to Gatework appear in this file. The format follows the Keep a Changelog convention. This project uses semantic versioning. +## [0.16.0.0] - 2026-08-04 + +### Added + +- Add the `BUF` gate for non-inverting signal transfer. +- Pass low, high, and unknown values through `BUF`. +- Convert floating `z` input to unknown `x` inside `BUF`. +- Support `BUF` on buses, modules, and delayed gate paths. +- Add a buffer waveform fixture, golden VCD, deterministic tests, and a QuickCheck property. + +### Changed + +- Bump the package version to 0.16.0.0. + ## [0.15.0.0] - 2026-08-04 ### Added diff --git a/README.md b/README.md index fad869c..f0becc5 100644 --- a/README.md +++ b/README.md @@ -58,6 +58,7 @@ You can do these tasks: - Watch a flip-flop output commit after its clock-to-output delay. - Capture data at the clock edge, not at the commit time. - Delay an asserted reset by the same amount. +- Use a non-inverting `BUF` gate for known and unknown signal paths. ## Architecture @@ -322,6 +323,35 @@ The run reports a pass only when every assertion holds. | 4 | 1 | 0 | 1 | 0 | 0 | | 6 | 0 | 0 | 1 | 1 | 1 | +## Buffer gate demo + +Run a direct buffer and a delayed buffer. + +```powershell +cabal run gatework -- --netlist fixtures/buffer.net --duration 8 --output buffer.vcd --set d=0 --at 2 d=1 --at 4 d=0 --at 6 d=z +``` + +The command writes this output: + +```text +Wrote buffer.vcd +Signals: 3 +Duration: 8 time units +Assertions: 9 passed +``` + +`BUF` passes low, high, and unknown values. +It maps a floating `z` input to `x`, because ordinary gates read floating inputs as unknown. +The delayed instance applies the existing gate delay rules. + +| Time | d | y | delayed | +| --- | --- | --- | --- | +| 0 | 0 | 0 | 0 | +| 2 | 1 | 1 | 0 | +| 4 | 0 | 0 | 1 | +| 6 | z | x | 0 | +| 8 | z | x | x | + ## Hierarchical adder demo Run the hierarchical ripple-carry adder. @@ -930,6 +960,31 @@ The output `q` commits to 1 at time 4. The reset rises at time 14. The output `q` stays 1 until the reset commit lands at time 16. +The file `fixtures/buffer.golden.vcd` holds the buffer demo waveform. +Its timeline shows direct transfer, delayed transfer, and floating-input handling: + +```text +#0 +0! +0" +0# +#2 +1! +1" +#4 +0! +0" +1# +#6 +z! +x" +0# +#8 +x# +``` + +Here `!` is `d`, `"` is `y`, and `#` is `delayed`. + ## Netlist format Use one declaration per line. @@ -948,7 +1003,7 @@ gate AND combine (n,b) -> y dff state clock=clk d=a q=state_q init=0 ``` -Supported gates are AND, OR, XOR, NAND, NOR, XNOR, NOT, and TRIBUF. +Supported gates are AND, OR, XOR, NAND, NOR, XNOR, NOT, BUF, and TRIBUF. NAND, NOR, and XNOR use two inputs. A gate output must have a `wire` or `output` declaration. A flip-flop uses `clock=`, `d=`, and `q=` fields. @@ -957,6 +1012,14 @@ It accepts an optional `tco=` clock-to-output delay field. Flip-flop clocks must be declared `clock` signals. Clock periods use even integers of at least two. +The `BUF` gate is a non-inverting buffer. +It passes low, high, and unknown values. +It converts a floating `z` input to unknown `x`. + +```text +gate BUF pass (d) -> y +``` + The `TRIBUF` gate is a tri-state buffer. Its first input is the data signal. Its second input is the enable signal. @@ -1252,6 +1315,7 @@ Deterministic tests also cover gate delay parsing and invalid delay fields. Deterministic tests also cover delayed transitions, delay accumulation, zero-delay behavior, multi-driver delays, and the initial settle. Deterministic tests also cover rise and fall delay parsing, conflict rules, direction-specific transitions, and the asymmetric delay demo. Deterministic tests also cover clock-to-output delay parsing, invalid tco fields, delayed commits, edge capture, delayed reset, wide register commits, and the golden output. +Deterministic tests also cover BUF truth values, bus behavior, delayed buffer behavior, and the buffer golden output. QuickCheck properties cover gate algebra, full adder correctness, scheduled input sampling, reset sampling, register width, and assertion soundness. QuickCheck properties also compare the hierarchical adder and counter with their flat versions. QuickCheck properties also cover the four-state model and the tri-state buffer truth table. @@ -1264,6 +1328,7 @@ QuickCheck properties also compare a clock-to-output flip-flop with a delayed re QuickCheck properties also compare the counter report with the simulated waveform. QuickCheck properties also compare whole-bus input values with per-bit reference values. QuickCheck properties also compare every VCD vector value with the per-bit waveform. +QuickCheck properties also cover BUF behavior across all four logic values. QuickCheck runs one hundred random cases for each property. The gate properties cover the complete truth table. @@ -1275,7 +1340,8 @@ The entry-point property shows that both simulation entry points produce identic The assertion property shows that real values pass and inverted values fail. The hierarchy property shows that the hierarchical circuits match the flat circuits. The four-state property shows that the gates keep their two-state behavior for known inputs. -The buffer properties show that an enabled buffer passes data and a disabled buffer floats. +The tri-state buffer property shows that an enabled driver passes data and a disabled driver floats. +The BUF property shows that direct transfer preserves known values and maps floating input to unknown. The bus XOR property compares a bus gate with per-bit evaluation. The bus register property compares each register bit with a reference value. The bus hierarchy property shows that a bus module matches its flat circuit. @@ -1288,8 +1354,9 @@ The asymmetric-delay property compares each output sample with the directional r ## Test status -All tests pass on GHC 9.6.7 with Cabal 3.14 in the bundled container. -The CI workflow runs the same checks on Ubuntu with GHC 9.6.6. +The previous release passed on GHC 9.6.7 with Cabal 3.14 in the bundled container. +This workspace could not run Cabal because the executable is unavailable. +The CI workflow runs the checks on Ubuntu with GHC 9.6.6. Golden tests compare each fixture VCD with its golden file. The golden report test compares the counter report table with its golden file. CI runs every demo and compares its output with the golden file. @@ -1299,6 +1366,7 @@ CI runs the four-state vector demo and compares it with its golden file. CI runs the gate delay demo and compares it with its golden file. CI runs the asymmetric delay demo and compares it with its golden file. CI runs the clock-to-output delay demo and compares it with its golden file. +CI runs the buffer demo and compares it with its golden file. CI confirms that a missing library file stops the run. CI confirms that an invalid gate delay stops the run. @@ -1306,6 +1374,7 @@ CI confirms that an invalid gate delay stops the run. The simulator uses four logic values: low, high, unknown, and floating. A floating value reads as unknown inside a gate. +The BUF gate preserves low, high, and unknown values. Several gates can drive one wire. The simulator resolves the driver values into one wire value. Resolution treats z as neutral and known values as dominant. @@ -1359,6 +1428,7 @@ The report prints every signal in the stable signal order. ## Roadmap +Release 0.16.0.0 completed the BUF gate and its waveform evidence. Release 0.15.0.0 completed the clock-to-output delay for flip-flops. Release 0.14.0.0 completed separate rise and fall gate delays. Release 0.13.0.0 completed configurable gate delays. @@ -1376,7 +1446,7 @@ Release 0.2.0.0 completed scheduled input transitions. Remaining work: -1. Add a buffer gate to the gate library. +1. Expand the gate library with additional circuit primitives. ## License diff --git a/fixtures/adder.golden.vcd b/fixtures/adder.golden.vcd index c32efb7..98eebee 100644 --- a/fixtures/adder.golden.vcd +++ b/fixtures/adder.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/assert.golden.vcd b/fixtures/assert.golden.vcd index 2189e75..c0434ff 100644 --- a/fixtures/assert.golden.vcd +++ b/fixtures/assert.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $comment assert y = 1 at 0 diff --git a/fixtures/asymdelay.golden.vcd b/fixtures/asymdelay.golden.vcd index 675f2bf..c1f8327 100644 --- a/fixtures/asymdelay.golden.vcd +++ b/fixtures/asymdelay.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $comment assert y = 1 at 0 diff --git a/fixtures/buffer.golden.vcd b/fixtures/buffer.golden.vcd new file mode 100644 index 0000000..80237f3 --- /dev/null +++ b/fixtures/buffer.golden.vcd @@ -0,0 +1,41 @@ +$date + generated deterministically by gatework +$end +$version + gatework 0.16.0.0 +$end +$comment + assert y = 0 at 0 + assert delayed = 0 at 0 + assert y = 1 at 2 + assert delayed = 0 at 2 + assert y = 0 at 4 + assert delayed = 1 at 4 + assert y = x at 6 + assert delayed = 0 at 6 + assert delayed = x at 8 +$end +$timescale 1ns $end +$scope module gatework $end +$var wire 1 ! d $end +$var wire 1 " y $end +$var wire 1 # delayed $end +$upscope $end +$enddefinitions $end +#0 +0! +0" +0# +#2 +1! +1" +#4 +0! +0" +1# +#6 +z! +x" +0# +#8 +x# \ No newline at end of file diff --git a/fixtures/buffer.net b/fixtures/buffer.net new file mode 100644 index 0000000..dc58f2b --- /dev/null +++ b/fixtures/buffer.net @@ -0,0 +1,17 @@ +# A plain buffer preserves known values and reads floating input as unknown. +input d +output y +output delayed +wire y +wire delayed +gate BUF pass (d) -> y +gate BUF slow (d) -> delayed delay=2 +assert y = 0 at 0 +assert delayed = 0 at 0 +assert y = 1 at 2 +assert delayed = 0 at 2 +assert y = 0 at 4 +assert delayed = 1 at 4 +assert y = x at 6 +assert delayed = 0 at 6 +assert delayed = x at 8 \ No newline at end of file diff --git a/fixtures/bus.golden.vcd b/fixtures/bus.golden.vcd index d933094..8dd94dc 100644 --- a/fixtures/bus.golden.vcd +++ b/fixtures/bus.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $comment assert x[0] = 1 at 0 diff --git a/fixtures/counter.golden.vcd b/fixtures/counter.golden.vcd index eaa139b..dc12975 100644 --- a/fixtures/counter.golden.vcd +++ b/fixtures/counter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/delay.golden.vcd b/fixtures/delay.golden.vcd index 012b3c2..ba9500a 100644 --- a/fixtures/delay.golden.vcd +++ b/fixtures/delay.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $comment assert x = 1 at 0 diff --git a/fixtures/gates.golden.vcd b/fixtures/gates.golden.vcd index 09c7768..6fd0a48 100644 --- a/fixtures/gates.golden.vcd +++ b/fixtures/gates.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $comment assert nand_out = 1 at 0 diff --git a/fixtures/haddader.golden.vcd b/fixtures/haddader.golden.vcd index d3e3ad9..35564f0 100644 --- a/fixtures/haddader.golden.vcd +++ b/fixtures/haddader.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/hcounter.golden.vcd b/fixtures/hcounter.golden.vcd index 1f57be4..4e4fe15 100644 --- a/fixtures/hcounter.golden.vcd +++ b/fixtures/hcounter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/libadder.golden.vcd b/fixtures/libadder.golden.vcd index d3e3ad9..35564f0 100644 --- a/fixtures/libadder.golden.vcd +++ b/fixtures/libadder.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/reg2.golden.vcd b/fixtures/reg2.golden.vcd index 70d03af..1a9fba9 100644 --- a/fixtures/reg2.golden.vcd +++ b/fixtures/reg2.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/register.golden.vcd b/fixtures/register.golden.vcd index 200b272..147166b 100644 --- a/fixtures/register.golden.vcd +++ b/fixtures/register.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/reset.golden.vcd b/fixtures/reset.golden.vcd index cccad76..744f30e 100644 --- a/fixtures/reset.golden.vcd +++ b/fixtures/reset.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/shared.golden.vcd b/fixtures/shared.golden.vcd index 96756a1..ffb405c 100644 --- a/fixtures/shared.golden.vcd +++ b/fixtures/shared.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/tco.golden.vcd b/fixtures/tco.golden.vcd index f84414e..2587cd3 100644 --- a/fixtures/tco.golden.vcd +++ b/fixtures/tco.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $comment assert q = 0 at 0 diff --git a/fixtures/tristate.golden.vcd b/fixtures/tristate.golden.vcd index 29cf0aa..8f4c0d6 100644 --- a/fixtures/tristate.golden.vcd +++ b/fixtures/tristate.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/unknown.golden.vcd b/fixtures/unknown.golden.vcd index 611b1e9..b1e8046 100644 --- a/fixtures/unknown.golden.vcd +++ b/fixtures/unknown.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $comment assert q = x at 0 diff --git a/fixtures/vector4.golden.vcd b/fixtures/vector4.golden.vcd index 3a91056..745a4b1 100644 --- a/fixtures/vector4.golden.vcd +++ b/fixtures/vector4.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.16.0.0 $end $comment assert x[0] = 1 at 0 diff --git a/gatework.cabal b/gatework.cabal index 7f0b98a..8ce3205 100644 --- a/gatework.cabal +++ b/gatework.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: gatework -version: 0.15.0.0 +version: 0.16.0.0 synopsis: Event-driven digital logic simulation in Haskell description: Gatework parses typed netlists, runs combinational gates and D @@ -17,6 +17,7 @@ description: Buses render as multi-bit vectors in the VCD timeline. A gate can declare a delay with the delay=N field. A gate can declare separate rise and fall delays. + A one-input BUF gate transfers known values and maps floating input to unknown. The scheduler delays each gate transition by the declared amount. A flip-flop can declare a clock-to-output delay with the tco=N field. The scheduler commits each flip-flop output after that delay. diff --git a/src/Gatework/Logic.hs b/src/Gatework/Logic.hs index 4dabde6..130edf3 100644 --- a/src/Gatework/Logic.hs +++ b/src/Gatework/Logic.hs @@ -14,7 +14,7 @@ import Data.List (foldl') data Logic = Low | High | Undefined | TriState deriving (Eq, Ord, Read, Show) -data GateType = And | Or | Xor | Not | Nand | Nor | Xnor | Tribuf +data GateType = And | Or | Xor | Not | Nand | Nor | Xnor | Buf | Tribuf deriving (Eq, Ord, Read, Show) gateArity :: GateType -> Int @@ -25,6 +25,7 @@ gateArity Not = 1 gateArity Nand = 2 gateArity Nor = 2 gateArity Xnor = 2 +gateArity Buf = 1 gateArity Tribuf = 2 parseGateType :: String -> Maybe GateType @@ -36,6 +37,7 @@ parseGateType value = case map toLower value of "nand" -> Just Nand "nor" -> Just Nor "xnor" -> Just Xnor + "buf" -> Just Buf "tribuf" -> Just Tribuf _ -> Nothing @@ -79,6 +81,9 @@ evalGate Xnor inputs evalGate Not inputs = case inputs of input : _ -> invert input [] -> Undefined +evalGate Buf inputs = case inputs of + [input] -> bufferValue input + _ -> Undefined evalGate Tribuf inputs = case inputs of [dataValue, enable] -> tribufValue dataValue enable _ -> Undefined @@ -92,6 +97,10 @@ invert High = Low invert Undefined = Undefined invert TriState = Undefined +bufferValue :: Logic -> Logic +bufferValue TriState = Undefined +bufferValue value = value + tribufValue :: Logic -> Logic -> Logic tribufValue dataValue enable = case enable of Low -> TriState diff --git a/test/Spec.hs b/test/Spec.hs index 332809e..303b65d 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -158,6 +158,10 @@ main = do deterministic <- sequence [ testParser , testParserAcceptsCommentsAndBlankLines + , testBufferTruth + , testBufferFixture + , testBufferBus + , testGoldenBufferVCD , testParserRejectsUnknownGate , testParserRejectsWrongArity , testParserRejectsEmptyInputs @@ -343,6 +347,7 @@ main = do , ("four-state gates match the two-state reference", quickCheckResult propTwoStateMatchesReference) , ("undefined inputs commute in binary gates", quickCheckResult propUndefinedCommutative) , ("TRIBUF follows its truth table", quickCheckResult propTribufTruth) + , ("BUF follows its four-state truth table", quickCheckResult propBufferTruth) , ("an enabled buffer passes known data", quickCheckResult propTribufEnable) , ("tri-state fixture stays consistent", quickCheckResult (propTribufFixtureSound tristate)) , ("unknown fixture starts unclocked", quickCheckResult (propUnknownFixtureSampling unknown)) @@ -1123,6 +1128,66 @@ testNandNorXnorTruth = , evalGate Xnor [High, High] == High ] +testBufferTruth :: IO Bool +testBufferTruth = + check "BUF passes known values and maps floating input to unknown" $ + and + [ evalGate Buf [Low] == Low + , evalGate Buf [High] == High + , evalGate Buf [Undefined] == Undefined + , evalGate Buf [TriState] == Undefined + , evalGate Buf [] == Undefined + ] + +testBufferFixture :: IO Bool +testBufferFixture = do + source <- readFile "fixtures/buffer.net" + case parseNetlist source of + Left _ -> check "buffer fixture simulates delayed copies" False + Right netlist -> check "buffer fixture simulates delayed copies" $ case + simulateWithScheduledInputs netlist [ ("d", Low) ] + [(2, "d", High), (4, "d", Low), (6, "d", TriState)] 8 of + Right simulation -> + null (simulationFailures simulation) + && length (simulationAssertions simulation) == 9 + && valueAt simulation "y" 0 == Low + && valueAt simulation "y" 2 == High + && valueAt simulation "y" 6 == Undefined + && valueAt simulation "delayed" 2 == Low + && valueAt simulation "delayed" 4 == High + && valueAt simulation "delayed" 6 == Low + && valueAt simulation "delayed" 8 == Undefined + Left _ -> False + +testBufferBus :: IO Bool +testBufferBus = case parseNetlist (unlines + [ "input a[4]" + , "output y[4]" + , "wire y[4]" + , "gate BUF copy (a) -> y" + ]) of + Left _ -> check "BUF applies bitwise across a bus" False + Right netlist -> check "BUF applies bitwise across a bus" $ case + simulateWithInputs netlist (busInputs "a" 9 4) 0 of + Right simulation -> + valueAt simulation "y[0]" 0 == High + && valueAt simulation "y[1]" 0 == Low + && valueAt simulation "y[2]" 0 == Low + && valueAt simulation "y[3]" 0 == High + Left _ -> False + +testGoldenBufferVCD :: IO Bool +testGoldenBufferVCD = do + source <- readFile "fixtures/buffer.net" + golden <- readFile "fixtures/buffer.golden.vcd" + let actual = do + netlist <- parseNetlist source + simulation <- + simulateWithScheduledInputs netlist [ ("d", Low) ] + [(2, "d", High), (4, "d", Low), (6, "d", TriState)] 8 + pure (renderVCD simulation) + check "buffer VCD matches golden file" (actual == Right golden) + testGatesFixture :: IO Bool testGatesFixture = do source <- readFile "fixtures/gates.net" @@ -2506,6 +2571,9 @@ evalTwoState Xnor inputs = invertTwo (foldl' xorTwo Low inputs) evalTwoState Not inputs = case inputs of input : _ -> invertTwo input [] -> Low +evalTwoState Buf inputs = case inputs of + [input] -> if input == High then High else Low + _ -> Low evalTwoState Tribuf _ = Low xorTwo :: Logic -> Logic -> Logic @@ -2527,6 +2595,7 @@ propTwoStateMatchesReference (Known left) (Known right) = , evalGate Nor [left, right] == evalTwoState Nor [left, right] , evalGate Xnor [left, right] == evalTwoState Xnor [left, right] , evalGate Not [left] == evalTwoState Not [left] + , evalGate Buf [left] == evalTwoState Buf [left] ] propUndefinedCommutative :: Known -> Bool @@ -2556,6 +2625,10 @@ propTribufEnable (Known dataValue) = evalGate Tribuf [dataValue, Low] == TriState && evalGate Tribuf [dataValue, High] == dataValue +propBufferTruth :: FourState -> Bool +propBufferTruth (FourState value) = + evalGate Buf [value] == if value == TriState then Undefined else value + propTribufFixtureSound :: Netlist -> Property propTribufFixtureSound netlist = forAll (elements [Low, High]) $ \dataValue -> From d6df1afd40ebad62b0ecfeb8d80e5d865186ccd0 Mon Sep 17 00:00:00 2001 From: DanieCuevas <43822444+DanielCuevas1208@users.noreply.github.com> Date: Tue, 4 Aug 2026 04:03:06 -0700 Subject: [PATCH 2/2] feat: extend gatework --- .github/workflows/ci.yml | 4 ++ CHANGELOG.md | 17 ++++++ README.md | 53 +++++++++++++++++- fixtures/adder.golden.vcd | 2 +- fixtures/assert.golden.vcd | 2 +- fixtures/asymdelay.golden.vcd | 2 +- fixtures/buffer.golden.vcd | 4 +- fixtures/bus.golden.vcd | 2 +- fixtures/counter.golden.vcd | 2 +- fixtures/delay.golden.vcd | 2 +- fixtures/gates.golden.vcd | 2 +- fixtures/haddader.golden.vcd | 2 +- fixtures/hcounter.golden.vcd | 2 +- fixtures/libadder.golden.vcd | 2 +- fixtures/mux.golden.vcd | 46 ++++++++++++++++ fixtures/mux.net | 19 +++++++ fixtures/reg2.golden.vcd | 2 +- fixtures/register.golden.vcd | 2 +- fixtures/reset.golden.vcd | 2 +- fixtures/shared.golden.vcd | 2 +- fixtures/tco.golden.vcd | 2 +- fixtures/tristate.golden.vcd | 2 +- fixtures/unknown.golden.vcd | 2 +- fixtures/vector4.golden.vcd | 2 +- gatework.cabal | 3 +- src/Gatework/Logic.hs | 19 ++++++- test/Spec.hs | 101 ++++++++++++++++++++++++++++++++++ 27 files changed, 277 insertions(+), 25 deletions(-) create mode 100644 fixtures/mux.golden.vcd create mode 100644 fixtures/mux.net diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index bae1771..e81d4d7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -112,6 +112,10 @@ jobs: run: cabal run gatework -- --netlist fixtures/buffer.net --duration 8 --output /tmp/buffer.vcd --set d=0 --at 2 d=1 --at 4 d=0 --at 6 d=z - name: Compare the buffer demo with the golden file run: diff fixtures/buffer.golden.vcd /tmp/buffer.vcd + - name: Run the MUX demo + run: cabal run gatework -- --netlist fixtures/mux.net --duration 10 --output /tmp/mux.vcd --set d0=0,d1=1,sel=0 --at 2 sel=1 --at 4 sel=x --at 6 d0=1,d1=1 --at 8 sel=z + - name: Compare the MUX demo with the golden file + run: diff fixtures/mux.golden.vcd /tmp/mux.vcd - name: Confirm a missing library file stops the run run: | if cabal run gatework -- --netlist fixtures/libadder.net --library fixtures/missing.net --duration 0 --output /tmp/none.vcd 2>/tmp/none.log; then diff --git a/CHANGELOG.md b/CHANGELOG.md index 649627f..200e122 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,23 @@ All notable changes to Gatework appear in this file. The format follows the Keep a Changelog convention. This project uses semantic versioning. +## [0.17.0.0] - 2026-08-04 + +### Added + +- Add the `MUX` gate with `(d0,d1,sel)` inputs. +- Select `d0` when `sel` is low. +- Select `d1` when `sel` is high. +- Resolve an unknown selector to the common branch value when both branches agree. +- Convert floating selected data to unknown. +- Support `MUX` on buses, modules, and delayed gate paths. +- Add a multiplexer waveform fixture, golden VCD, deterministic tests, and a QuickCheck property. + +### Fixed + +- Add the missing final newline to the buffer golden VCD. +- Bump the package version to 0.17.0.0. + ## [0.16.0.0] - 2026-08-04 ### Added diff --git a/README.md b/README.md index f0becc5..8c216f4 100644 --- a/README.md +++ b/README.md @@ -59,6 +59,7 @@ You can do these tasks: - Capture data at the clock edge, not at the commit time. - Delay an asserted reset by the same amount. - Use a non-inverting `BUF` gate for known and unknown signal paths. +- Select data with a three-input `MUX` gate. ## Architecture @@ -352,6 +353,38 @@ The delayed instance applies the existing gate delay rules. | 6 | z | x | 0 | | 8 | z | x | x | +## Multiplexer gate demo + +Run the multiplexer demo. + +```powershell +cabal run gatework -- --netlist fixtures/mux.net --duration 10 --output mux.vcd --set d0=0,d1=1,sel=0 --at 2 sel=1 --at 4 sel=x --at 6 d0=1,d1=1 --at 8 sel=z +``` + +The command writes this output: + +```text +Wrote mux.vcd +Signals: 5 +Duration: 10 time units +Assertions: 9 passed +``` + +`MUX` uses `(d0,d1,sel)` input order. +A low selector chooses `d0`. +A high selector chooses `d1`. +An unknown selector returns the common branch value when both branches agree. +A floating selected value becomes `x`. +The delayed instance shows the same behavior two time units later. + +| Time | d0 | d1 | sel | y | delayed | +| --- | --- | --- | --- | --- | --- | +| 0 | 0 | 1 | 0 | 0 | 0 | +| 2 | 0 | 1 | 1 | 1 | 0 | +| 4 | 0 | 1 | x | x | 1 | +| 6 | 1 | 1 | x | 1 | x | +| 8 | 1 | 1 | z | 1 | 1 | + ## Hierarchical adder demo Run the hierarchical ripple-carry adder. @@ -1003,7 +1036,7 @@ gate AND combine (n,b) -> y dff state clock=clk d=a q=state_q init=0 ``` -Supported gates are AND, OR, XOR, NAND, NOR, XNOR, NOT, BUF, and TRIBUF. +Supported gates are AND, OR, XOR, NAND, NOR, XNOR, NOT, BUF, MUX, and TRIBUF. NAND, NOR, and XNOR use two inputs. A gate output must have a `wire` or `output` declaration. A flip-flop uses `clock=`, `d=`, and `q=` fields. @@ -1020,6 +1053,16 @@ It converts a floating `z` input to unknown `x`. gate BUF pass (d) -> y ``` +The `MUX` gate selects one of two data inputs. +Its first input is `d0`. +Its second input is `d1`. +Its third input is `sel`. +A low selector selects the first input. +A high selector selects the second input. +An unknown selector compares the normalized data values. +Equal values pass through. +Different values produce `x`. + The `TRIBUF` gate is a tri-state buffer. Its first input is the data signal. Its second input is the enable signal. @@ -1315,7 +1358,7 @@ Deterministic tests also cover gate delay parsing and invalid delay fields. Deterministic tests also cover delayed transitions, delay accumulation, zero-delay behavior, multi-driver delays, and the initial settle. Deterministic tests also cover rise and fall delay parsing, conflict rules, direction-specific transitions, and the asymmetric delay demo. Deterministic tests also cover clock-to-output delay parsing, invalid tco fields, delayed commits, edge capture, delayed reset, wide register commits, and the golden output. -Deterministic tests also cover BUF truth values, bus behavior, delayed buffer behavior, and the buffer golden output. +Deterministic tests also cover BUF and MUX truth values, bus behavior, delayed paths, and their golden outputs. QuickCheck properties cover gate algebra, full adder correctness, scheduled input sampling, reset sampling, register width, and assertion soundness. QuickCheck properties also compare the hierarchical adder and counter with their flat versions. QuickCheck properties also cover the four-state model and the tri-state buffer truth table. @@ -1328,7 +1371,7 @@ QuickCheck properties also compare a clock-to-output flip-flop with a delayed re QuickCheck properties also compare the counter report with the simulated waveform. QuickCheck properties also compare whole-bus input values with per-bit reference values. QuickCheck properties also compare every VCD vector value with the per-bit waveform. -QuickCheck properties also cover BUF behavior across all four logic values. +QuickCheck properties also cover BUF behavior and MUX selection across all four logic values. QuickCheck runs one hundred random cases for each property. The gate properties cover the complete truth table. @@ -1342,6 +1385,7 @@ The hierarchy property shows that the hierarchical circuits match the flat circu The four-state property shows that the gates keep their two-state behavior for known inputs. The tri-state buffer property shows that an enabled driver passes data and a disabled driver floats. The BUF property shows that direct transfer preserves known values and maps floating input to unknown. +The MUX property shows that an unknown selector passes equal branches and rejects different branches. The bus XOR property compares a bus gate with per-bit evaluation. The bus register property compares each register bit with a reference value. The bus hierarchy property shows that a bus module matches its flat circuit. @@ -1367,6 +1411,7 @@ CI runs the gate delay demo and compares it with its golden file. CI runs the asymmetric delay demo and compares it with its golden file. CI runs the clock-to-output delay demo and compares it with its golden file. CI runs the buffer demo and compares it with its golden file. +CI runs the MUX demo and compares it with its golden file. CI confirms that a missing library file stops the run. CI confirms that an invalid gate delay stops the run. @@ -1375,6 +1420,7 @@ CI confirms that an invalid gate delay stops the run. The simulator uses four logic values: low, high, unknown, and floating. A floating value reads as unknown inside a gate. The BUF gate preserves low, high, and unknown values. +The MUX gate returns `x` when an unknown selector chooses different branches. Several gates can drive one wire. The simulator resolves the driver values into one wire value. Resolution treats z as neutral and known values as dominant. @@ -1428,6 +1474,7 @@ The report prints every signal in the stable signal order. ## Roadmap +Release 0.17.0.0 completed the MUX gate and its waveform evidence. Release 0.16.0.0 completed the BUF gate and its waveform evidence. Release 0.15.0.0 completed the clock-to-output delay for flip-flops. Release 0.14.0.0 completed separate rise and fall gate delays. diff --git a/fixtures/adder.golden.vcd b/fixtures/adder.golden.vcd index 98eebee..b920082 100644 --- a/fixtures/adder.golden.vcd +++ b/fixtures/adder.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/assert.golden.vcd b/fixtures/assert.golden.vcd index c0434ff..4ea4a51 100644 --- a/fixtures/assert.golden.vcd +++ b/fixtures/assert.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $comment assert y = 1 at 0 diff --git a/fixtures/asymdelay.golden.vcd b/fixtures/asymdelay.golden.vcd index c1f8327..bb0b1c8 100644 --- a/fixtures/asymdelay.golden.vcd +++ b/fixtures/asymdelay.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $comment assert y = 1 at 0 diff --git a/fixtures/buffer.golden.vcd b/fixtures/buffer.golden.vcd index 80237f3..ae7d7e7 100644 --- a/fixtures/buffer.golden.vcd +++ b/fixtures/buffer.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $comment assert y = 0 at 0 @@ -38,4 +38,4 @@ z! x" 0# #8 -x# \ No newline at end of file +x# diff --git a/fixtures/bus.golden.vcd b/fixtures/bus.golden.vcd index 8dd94dc..6cea88b 100644 --- a/fixtures/bus.golden.vcd +++ b/fixtures/bus.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $comment assert x[0] = 1 at 0 diff --git a/fixtures/counter.golden.vcd b/fixtures/counter.golden.vcd index dc12975..a383952 100644 --- a/fixtures/counter.golden.vcd +++ b/fixtures/counter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/delay.golden.vcd b/fixtures/delay.golden.vcd index ba9500a..fcc7239 100644 --- a/fixtures/delay.golden.vcd +++ b/fixtures/delay.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $comment assert x = 1 at 0 diff --git a/fixtures/gates.golden.vcd b/fixtures/gates.golden.vcd index 6fd0a48..7c09db4 100644 --- a/fixtures/gates.golden.vcd +++ b/fixtures/gates.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $comment assert nand_out = 1 at 0 diff --git a/fixtures/haddader.golden.vcd b/fixtures/haddader.golden.vcd index 35564f0..afbb813 100644 --- a/fixtures/haddader.golden.vcd +++ b/fixtures/haddader.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/hcounter.golden.vcd b/fixtures/hcounter.golden.vcd index 4e4fe15..719bcf3 100644 --- a/fixtures/hcounter.golden.vcd +++ b/fixtures/hcounter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/libadder.golden.vcd b/fixtures/libadder.golden.vcd index 35564f0..afbb813 100644 --- a/fixtures/libadder.golden.vcd +++ b/fixtures/libadder.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/mux.golden.vcd b/fixtures/mux.golden.vcd new file mode 100644 index 0000000..cffcb87 --- /dev/null +++ b/fixtures/mux.golden.vcd @@ -0,0 +1,46 @@ +$date + generated deterministically by gatework +$end +$version + gatework 0.17.0.0 +$end +$comment + assert y = 0 at 0 + assert delayed = 0 at 0 + assert y = 1 at 2 + assert delayed = 0 at 2 + assert y = x at 4 + assert delayed = 1 at 4 + assert y = 1 at 6 + assert delayed = x at 6 + assert delayed = 1 at 8 +$end +$timescale 1ns $end +$scope module gatework $end +$var wire 1 ! d0 $end +$var wire 1 " d1 $end +$var wire 1 # sel $end +$var wire 1 $ y $end +$var wire 1 % delayed $end +$upscope $end +$enddefinitions $end +#0 +0! +1" +0# +0$ +0% +#2 +1# +1$ +#4 +x# +x$ +1% +#6 +1! +1$ +x% +#8 +z# +1% diff --git a/fixtures/mux.net b/fixtures/mux.net new file mode 100644 index 0000000..f5880a7 --- /dev/null +++ b/fixtures/mux.net @@ -0,0 +1,19 @@ +# A multiplexer selects data and resolves equal branches when the selector is unknown. +input d0 +input d1 +input sel +output y +output delayed +wire y +wire delayed +gate MUX choose (d0,d1,sel) -> y +gate MUX slow (d0,d1,sel) -> delayed delay=2 +assert y = 0 at 0 +assert delayed = 0 at 0 +assert y = 1 at 2 +assert delayed = 0 at 2 +assert y = x at 4 +assert delayed = 1 at 4 +assert y = 1 at 6 +assert delayed = x at 6 +assert delayed = 1 at 8 diff --git a/fixtures/reg2.golden.vcd b/fixtures/reg2.golden.vcd index 1a9fba9..94c5ffc 100644 --- a/fixtures/reg2.golden.vcd +++ b/fixtures/reg2.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/register.golden.vcd b/fixtures/register.golden.vcd index 147166b..068bc93 100644 --- a/fixtures/register.golden.vcd +++ b/fixtures/register.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/reset.golden.vcd b/fixtures/reset.golden.vcd index 744f30e..d3c988c 100644 --- a/fixtures/reset.golden.vcd +++ b/fixtures/reset.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/shared.golden.vcd b/fixtures/shared.golden.vcd index ffb405c..7b99122 100644 --- a/fixtures/shared.golden.vcd +++ b/fixtures/shared.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/tco.golden.vcd b/fixtures/tco.golden.vcd index 2587cd3..ce97997 100644 --- a/fixtures/tco.golden.vcd +++ b/fixtures/tco.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $comment assert q = 0 at 0 diff --git a/fixtures/tristate.golden.vcd b/fixtures/tristate.golden.vcd index 8f4c0d6..c0a0eda 100644 --- a/fixtures/tristate.golden.vcd +++ b/fixtures/tristate.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/unknown.golden.vcd b/fixtures/unknown.golden.vcd index b1e8046..a4726a1 100644 --- a/fixtures/unknown.golden.vcd +++ b/fixtures/unknown.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $comment assert q = x at 0 diff --git a/fixtures/vector4.golden.vcd b/fixtures/vector4.golden.vcd index 745a4b1..de9077e 100644 --- a/fixtures/vector4.golden.vcd +++ b/fixtures/vector4.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.16.0.0 + gatework 0.17.0.0 $end $comment assert x[0] = 1 at 0 diff --git a/gatework.cabal b/gatework.cabal index 8ce3205..23d075d 100644 --- a/gatework.cabal +++ b/gatework.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: gatework -version: 0.16.0.0 +version: 0.17.0.0 synopsis: Event-driven digital logic simulation in Haskell description: Gatework parses typed netlists, runs combinational gates and D @@ -18,6 +18,7 @@ description: A gate can declare a delay with the delay=N field. A gate can declare separate rise and fall delays. A one-input BUF gate transfers known values and maps floating input to unknown. + A three-input MUX gate selects one data input and resolves equal unknown branches. The scheduler delays each gate transition by the declared amount. A flip-flop can declare a clock-to-output delay with the tco=N field. The scheduler commits each flip-flop output after that delay. diff --git a/src/Gatework/Logic.hs b/src/Gatework/Logic.hs index 130edf3..b28beab 100644 --- a/src/Gatework/Logic.hs +++ b/src/Gatework/Logic.hs @@ -14,7 +14,7 @@ import Data.List (foldl') data Logic = Low | High | Undefined | TriState deriving (Eq, Ord, Read, Show) -data GateType = And | Or | Xor | Not | Nand | Nor | Xnor | Buf | Tribuf +data GateType = And | Or | Xor | Not | Nand | Nor | Xnor | Buf | Mux | Tribuf deriving (Eq, Ord, Read, Show) gateArity :: GateType -> Int @@ -26,6 +26,7 @@ gateArity Nand = 2 gateArity Nor = 2 gateArity Xnor = 2 gateArity Buf = 1 +gateArity Mux = 3 gateArity Tribuf = 2 parseGateType :: String -> Maybe GateType @@ -38,6 +39,7 @@ parseGateType value = case map toLower value of "nor" -> Just Nor "xnor" -> Just Xnor "buf" -> Just Buf + "mux" -> Just Mux "tribuf" -> Just Tribuf _ -> Nothing @@ -84,6 +86,9 @@ evalGate Not inputs = case inputs of evalGate Buf inputs = case inputs of [input] -> bufferValue input _ -> Undefined +evalGate Mux inputs = case inputs of + [lowData, highData, select] -> muxValue lowData highData select + _ -> Undefined evalGate Tribuf inputs = case inputs of [dataValue, enable] -> tribufValue dataValue enable _ -> Undefined @@ -101,6 +106,18 @@ bufferValue :: Logic -> Logic bufferValue TriState = Undefined bufferValue value = value +muxValue :: Logic -> Logic -> Logic -> Logic +muxValue lowData highData select = case select of + Low -> bufferValue lowData + High -> bufferValue highData + Undefined -> commonValue + TriState -> commonValue + where + commonValue = + let normalizedLow = bufferValue lowData + normalizedHigh = bufferValue highData + in if normalizedLow == normalizedHigh then normalizedLow else Undefined + tribufValue :: Logic -> Logic -> Logic tribufValue dataValue enable = case enable of Low -> TriState diff --git a/test/Spec.hs b/test/Spec.hs index 303b65d..d718401 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -162,6 +162,10 @@ main = do , testBufferFixture , testBufferBus , testGoldenBufferVCD + , testMuxTruth + , testMuxFixture + , testMuxBus + , testGoldenMuxVCD , testParserRejectsUnknownGate , testParserRejectsWrongArity , testParserRejectsEmptyInputs @@ -348,6 +352,7 @@ main = do , ("undefined inputs commute in binary gates", quickCheckResult propUndefinedCommutative) , ("TRIBUF follows its truth table", quickCheckResult propTribufTruth) , ("BUF follows its four-state truth table", quickCheckResult propBufferTruth) + , ("MUX follows its four-state selection table", quickCheckResult propMuxTruth) , ("an enabled buffer passes known data", quickCheckResult propTribufEnable) , ("tri-state fixture stays consistent", quickCheckResult (propTribufFixtureSound tristate)) , ("unknown fixture starts unclocked", quickCheckResult (propUnknownFixtureSampling unknown)) @@ -1188,6 +1193,86 @@ testGoldenBufferVCD = do pure (renderVCD simulation) check "buffer VCD matches golden file" (actual == Right golden) +testMuxTruth :: IO Bool +testMuxTruth = + check "MUX selects data and resolves equal unknown branches" $ + and + [ evalGate Mux [Low, High, Low] == Low + , evalGate Mux [Low, High, High] == High + , evalGate Mux [Low, High, Undefined] == Undefined + , evalGate Mux [High, High, Undefined] == High + , evalGate Mux [TriState, TriState, TriState] == Undefined + , evalGate Mux [TriState, High, Low] == Undefined + , evalGate Mux [Low, High] == Undefined + ] + +testMuxFixture :: IO Bool +testMuxFixture = do + source <- readFile "fixtures/mux.net" + case parseNetlist source of + Left _ -> check "mux fixture simulates selection and delay" False + Right netlist -> check "mux fixture simulates selection and delay" $ case + simulateWithScheduledInputs netlist + [("d0", Low), ("d1", High), ("sel", Low)] + [ (2, "sel", High) + , (4, "sel", Undefined) + , (6, "d0", High) + , (6, "d1", High) + , (8, "sel", TriState) + ] + 10 of + Right simulation -> + null (simulationFailures simulation) + && length (simulationAssertions simulation) == 9 + && valueAt simulation "y" 0 == Low + && valueAt simulation "y" 2 == High + && valueAt simulation "y" 4 == Undefined + && valueAt simulation "y" 6 == High + && valueAt simulation "delayed" 2 == Low + && valueAt simulation "delayed" 4 == High + && valueAt simulation "delayed" 6 == Undefined + && valueAt simulation "delayed" 8 == High + Left _ -> False + +testMuxBus :: IO Bool +testMuxBus = case parseNetlist (unlines + [ "input a[4]" + , "input b[4]" + , "input sel[4]" + , "output y[4]" + , "wire y[4]" + , "gate MUX choose (a,b,sel) -> y" + ]) of + Left _ -> check "MUX applies selection bitwise across a bus" False + Right netlist -> check "MUX applies selection bitwise across a bus" $ case + simulateWithInputs netlist + (busInputs "a" 9 4 ++ busInputs "b" 6 4 ++ busInputs "sel" 3 4) + 0 of + Right simulation -> + valueAt simulation "y[0]" 0 == Low + && valueAt simulation "y[1]" 0 == High + && valueAt simulation "y[2]" 0 == Low + && valueAt simulation "y[3]" 0 == High + Left _ -> False + +testGoldenMuxVCD :: IO Bool +testGoldenMuxVCD = do + source <- readFile "fixtures/mux.net" + golden <- readFile "fixtures/mux.golden.vcd" + let actual = do + netlist <- parseNetlist source + simulation <- simulateWithScheduledInputs netlist + [("d0", Low), ("d1", High), ("sel", Low)] + [ (2, "sel", High) + , (4, "sel", Undefined) + , (6, "d0", High) + , (6, "d1", High) + , (8, "sel", TriState) + ] + 10 + pure (renderVCD simulation) + check "mux VCD matches golden file" (actual == Right golden) + testGatesFixture :: IO Bool testGatesFixture = do source <- readFile "fixtures/gates.net" @@ -2629,6 +2714,22 @@ propBufferTruth :: FourState -> Bool propBufferTruth (FourState value) = evalGate Buf [value] == if value == TriState then Undefined else value +propMuxTruth :: FourState -> FourState -> FourState -> Bool +propMuxTruth (FourState lowData) (FourState highData) (FourState select) = + evalGate Mux [lowData, highData, select] == expected + where + expected = case select of + Low -> normalize lowData + High -> normalize highData + Undefined -> commonValue + TriState -> commonValue + commonValue = + let normalizedLow = normalize lowData + normalizedHigh = normalize highData + in if normalizedLow == normalizedHigh then normalizedLow else Undefined + normalize TriState = Undefined + normalize value = value + propTribufFixtureSound :: Netlist -> Property propTribufFixtureSound netlist = forAll (elements [Low, High]) $ \dataValue ->